slides - Formal Systems Laboratory
Contents
1. The following module extends PEANO NAT with multiplication mod PEANO NAT is including PEANO NAT op mult Nat Nat gt Nat vars MN Nat eq mult zero M zero eq mult succ N M plus mult N M M endm Variable declarations are not imported 15 Putting it all Together We can now define our simple programming language and execute programs in this case PEANO NAT already had all the features mod SIMPLEST PROGRAMMING LANGUAGE is including PEANO NAT including PEANO NAT endm red mult succ succ zero mult succ succ zero succ succ zero The following is Maude s output reduce in SIMPLEST PROGRAMMING LANGUAGE mult succ succ zero mult succ succ zero succ succ zero rewrites 16 in Oms cpu Oms real rewrites second result Nat succ succ succ succ succ succ succ succ zero Even though this language is very simple and its syntax is ugly it 16 nevertheless shows a formal and executable definition of a language using equational logic and rewriting Our languages or analysis tools discussed in this class will be defined in a relatively similar manner though as expected they will be more involved For example a notion of state will be needed as well as several control structures 17 The Mix fix Notation Some operations are prefix but others are infix postfix or miz fix i e arguments can occur anywhere like in the case of if then_else2. in reasoning about the defined structures Exercise 1 Prove that any correct implementation of PEANO NAT should satisfy the property plus succ succ zero succ succ succ zero plus succ succ succ succ zero succ zero Equations can be applied from left to right or from right to left in reasoning which means that equational proofs may require exponential search thus making them theoretically intractable 13 Maude regards all equations as rewriting rules which means that they are applied only from left to right Thus any well formed term can either be derived infinitely often or be reduced to a normal form which cannot be reduced anymore by applying equations as rewriting rules Maude s command to reduce a term to its normal form is reduce or simply red Reduction will be made in the last defined module Maude gt reduce plus succ succ zero succ succ succ zero rewrites 3 in Oms cpu Oms real rewrites second result Nat succ succ succ succ succ zero Maude gt Millions of rewrites per second can be performed for which reason Maude can be almost used as a programming language 14 Importation Modules can be imported using the keywords protecting extending or including The difference between these importation modes is subtle and semantical rather than operational Fell free to use including the most general of them all the time and read the manual for more information
3. List eq rev I L append rev L I eq rev nil nil endm red rev 1 2345 k k gt should be 54321 35 The next module defines an operation which sorts a list of integers by insertion sort mod ISORT is protecting INT LIST OP isort IntList gt IntList vars I J Int var L IntList eq eq Op eq eq endm isort I L insert I isort L isort nil nil insert Int IntList gt IntList insert I J L if I gt J then J insert I L else I J L fi insert I nil I red isort 4 781469428327 9 xxx gt Should be 1223444677889 9 36 Defining Operations on Binary Trees Let us now consider a specification of binary trees where a tree can be either empty or an integer with a left and a right subtree mod TREE is protecting INT sort Tree op _ _ Tree Int Tree gt Tree op empty gt Tree endm We next define some operations on such trees also following the structure of the trees given by the two constructors above 37 The next simple operation simply mirrors a tree that is it recursively replaces each left subtree by the mirrored right subtree and vice versa mod MIRROR is protecting TREE op mirror Tree gt Tree vars L R Tree var I Int eq mirror L I R mirror R I mirror L eq mirror empty empty endm red mirror empty 3 empty 1 empty 5 empty 6 empty 2 empty k k gt should be empty 2 empty 6 empty 5 empty 1 empty 3
4. Maude supports mix fix notation by allowing the user to place the arguments of operations wherever one wants by using underscores Here are some examples op _ _ Int Int gt Int op _ Nat gt Nat op in_then_else_ BoolExp Stmt Stmt gt Stmt op _ _ _ BoolExp Exp Exp gt Exp Exercise 2 Rewrite PEANO NAT and PEANO NAT using mix fix notation What happens if you try to reduce an expression containing both _ and _ _ without parentheses 18 BNF Bachus Naur Form or CFG Context Free Grammar notations to describe the syntax of programming languages are very common We also used BNF to define the syntax of our simple language in the lectures on SOS From here on we can interchangeably use the mix fix notation instead of BNF or CFG so it is important to understand the relationship between the mix fix notation and BNF and CFG Exercise 3 Argue that the miz fix notation is equivalent to BNF and CFG Find an interesting simple example language and express its syntax using the miz fix notation BNF and production based CFG e g A gt AB a and B gt BA b Mix fix notation leads to an interesting problem that of parsing In the modified PEANO NAT of Ex 2 how do we parse x y z Maude has a command called parse which parses a term using the syntax of the most recently defined module To see all the parentheses first type the command set print with parentheses on see Subsection 17 5 in M
5. Programming Language Semantics Maude Grigore Rosu Department of Computer Science University of Illinois at Urbana Champaign General Information about Maude Maude is an executable specification language supporting rewrite logic specifications and having at its core a very fast rewrite engine We will use Maude as a platform for executing programming language definitions following various definitional styles Our short term objectives are 1 Learn how to use Maude 2 Show how various language definitional styles including the ones discussed so far or to be discussed big step and small step SOS MSOS reduction semantics with evaluation contexts the CHAM denotational semantics can be formally defined in Maude Maude s roots go back to Clear Edinburgh in 1970s and to OBJ Stanford Oxford in 1980s There are many other languages in the same family such as CafeOBJ Japan BOBJ San Diego California ELAN France Maude is currently being developed at Stanford Research Institute and at the University of Illinois at Urbana Champaign You can find more about Maude including a manual and many papers and examples on its webpage at http maude cs uiuc edu Due to the fact that Maude is executable interpreters for programming languages defined in Maude will be obtained for free which will be very useful for understanding refining and or changing the languages Moreover analysis tools for the specified l
6. anguages can also be obtained with little effort such as type checkers abstract interpreters or model checkers either by using analysis tools already provided by Maude or by deriving them explicitly from a language definition Devising formal semantic executable models of desired languages or tools before these are implemented is a crucial step towards a deep understanding of the language or tool In simplistic terms it is like devising a simulator for an expensive system before building the actual system However our simulators in this class will consist of exactly the semantics or the meaning of our desired systems defined using a very rigorous mathematical notation In the obtained formal executable model of a programming language executing a program will correspond to nothing but logical inference within the semantics of the language Maude is easy to install and should run on the assigned machines Type maude and you should see a welcome screen like the following bash maude NEEEET EET EET TETET ETT Welcome to Maude JIILETEET EET T EET EEIN Maude 2 5 built May 7 2010 18 28 32 Copyright 1997 2010 SRI International Wed Sep 1 10 16 41 2010 Maude gt You can download Maude from its web page at http maude cs uiuc edu Unix Linux is preferred but it also works on Windows Also save its user manual You will need it How to Use Maude Maude is interpreted just type your specifi
7. aude s manual 2 parse x y z reports ambiguous parsing Use parentheses to disambiguate parsing such as parse x y z To give priorities to certain operators in order to reduce the number of parentheses use precedence attribute when you declare operators op _ _ Int Int gt Int prec 33 op _ _ Int Int gt Int prec 31 The lower the precedence the stronger the binding 19 20 Maude has several buzltin modules including ones for natural and integer numbers The operations _ _ and _ _ have precedences 33 and 31 respectively in these builtin modules With these precedences one can parse as follows Maude gt set print with parentheses on Maude gt parse 10 2 3 Int 10 2 3 Sometimes especially when debugging the mixfix notation may be confusing If you wish to turn it off use the command Maude gt set print mixfix off Maude gt parse 10 2 3 Int _ _ 10 _ 2 3 21 Associativity Commutativity and Identity Attributes Many of the binary operations that will be used in this class will be associative A commutative C or have an identity I or combinations of these E g _ _ is associative commutative and has 0 as identity All these can be added as attributes to operations when declared op _t_ Int Int gt Int assoc comm id O prec 33 op _ _ Int Int gt Int assoc comm id 1 prec 31 Notice that each of the A C and I at
8. cations and commands Better way to use it 1 Type everything in one file say p maude 2 Start Maude 3 Include that file with the command in p or in p maude 4 Use quit or q to quit Specifications are introduced as modules or theories We will use only general modules in this class which have the syntax mod lt NAME gt is lt BODY gt endm The lt BODY gt can include e Importation of other modules e Sort and operation declarations forming the szgnature of that module this is the interface of that module to the outside world e Sentences We will use modules to define programming language features These features can be then imported by other modules which can extend them or use them to define other features A programming language will be also defined as a module namely one importing all the modules defining its desired features Let us exemplify this paradigm by defining the simplest programming language that we will see in this class It is so simple that it does not even deserve to be called a programming language but we do so for the sake of a uniform terminology The language specified in what follows defines natural numbers with addition and multiplication One module will define the feature addition and another will define the feature multiplication on top of addition 10 An Example Peano Natural Numbers The following defines natural number
9. empty 38 Searching in binary trees can be defined as follows mod SEARCH is protecting TREE op search Int Tree gt Bool vars I J Int vars LR Tree eq search I L I R eq search I L J R eq search I empty false true search I L or search I R owise endm red search 6 empty 3 empty 1 empty 5 empty 6 empty 2 empty k gt should be true red search 7 empty 3 empty 1 empty 5 empty 6 empty 2 empty k gt should be false Notice the use of the attribute owise for the second equation Exercise 6 Define search with only two equations by using the built in if _then_else_fi 39 Putting Together Trees and Lists We next define a module which imports both modules of trees and of lists on integers and defines an operation which takes a tree and returns the list of all integers in that tree in an infix traversal mod FLATTEN is protecting APPEND protecting TREE op flatten Tree gt IntList vars LR Tree var I Int eq flatten L I R append flatten L I flatten R eq flatten empty nil endm red flatten empty 3 empty 1 empty 5 empty 6 empty 2 empty gt Should be 3 15 6 2 Exercise 7 Do the same for prefix and for postfix traversals 40 Exercise 8 Write an executable specification in Maude that uses binary trees to sort lists of integers You should define an operation btsort IntList gt IntList which sorts the argument list of in
10. he concatenation of an integer to a list Let us next define several other important and useful operations on lists Notice that the definition of each operator treats each of the constructors separately 31 The following defines the usual length operator mod LENGTH is protecting INT LIST op length IntList gt Nat var I Int var L IntList eq length I L 1 length L O eq length nil endm red length 1 2345 gt should be 5 32 The following defines membership without speculating matching in fact this would not be possible anyway because concatenation is not defined associative as before mod IN is protecting INT LIST op _in_ Int IntList gt Bool vars I J Int var L IntList eq I in J L if I J then true else I in L fi eq I in nil false endm red 3 in 2 34 gt should be true red 3 in 3 4 5 gt should be true red 3 in 1 2 3 gt should be true red 3 in 1 2 4 gt should be false 33 The next operator appends two lists of integers mod APPEND is protecting INT LIST op append IntList IntList gt IntList var I Int vars Li L2 IntList eq append I Li L2 I append Li L2 eq append nil L2 L2 endm red append 1 2 3 4 5 6 7 8 k gt Should be 12345 6 7 8 34 The following imports APPEND and defines an operation which reverses a list mod REV is protecting APPEND op rev IntList gt IntList var I Int var L Int
11. ment Maude gt red 3 in2 34 result Bool true Maude gt red 3 in3 45 result Bool true Maude gt red 3 in 124 result Bool false By AI matching I L and L in the left hand side term of eq I 25 in L I L true can match any integer or lists of integers respectively including nil Since I can only be matched by 3 the other matches follow automatically The attribute owise in eq I in L false owise tells Maude to apply that equation only otherwise that is only if no other equation in this case the previous one only can be applied If one wants to define sets of integers then besides replacing the sort IntList probably by IntSet one has to declare the concatenation also commutative and one has to replace the first 2 equation by eq I in I L true Exercise 4 Define a Maude module called INT SET specifying sets of integers with membership union intersection and difference elements in one set and not in the other The matching modulo attributes are implemented very efficiently in Maude so you typically don t have to worry about efficiency 26 Built in Modules There are several built in modules We will use the following e BOOL Provides a sort Bool with two constants true false and basic boolean calculus together with if_then_else_fi and _ _ operations The later takes two terms reduces them to their normal forms and then returns true iff they a
12. re equal modulo ACI as appropriate otherwise it returns false e INT Provides a sort Int arbitrary large integers as constants of sort Int together with the usual operations on these e QID Provides a sort Qid together with arbitrary large quoted identifiers as constants of sort Qid of the form a b a larger identifier etc To see an existing module built in or not type the command Maude gt show module lt NAME gt 27 2 For example show module BOOL will output mod BOOL is protecting TRUTH op _and_ Bool Bool gt Bool assoc comm prec 55 op _or_ Bool Bool gt Bool assoc comm prec 59 op _xor_ Bool Bool gt Bool assoc comm prec 57 op not_ Bool gt Bool prec 53 op _implies_ Bool Bool gt Bool prec 61 gather e E vars A B C Bool eq true and A A eq false and A false eq AandA A eq false xor A A eq A xor A false eq not A A xor true eq A and B xor C A and B xor A and C eq A or B A and B xor A xorB eq A implies B not A xor A and B endm 22 Exercise 5 Use the command show module lt NAME gt on the three modules above and try to understand them 28 Constructor versus Defined Operations When we defined the operation plus on Peano natural numbers we defined it recursively on numbers of the form zero and succ N Why did we do that considering that PEANO NAT had declared three operations op zero gt Nat op succ Nat gt Na
13. s with successor and addition using Peano s axiomatization mod PEANO NAT is sort Nat op zero gt Nat op succ Nat gt Nat op plus Nat Nat gt Nat vars NM Nat eq plus zero M M eq plus succ N M succ plus N M endm Declarations are separated by periods which should typically have white spaces before and after 11 One sort Nat and three operations zero succ and plus form the signature of PEANO NAT Sorts are declared with the keywords sort or sorts and operations with op or ops The three operations have zero one and two arguments resp whose sorts are between and gt Operations of zero arguments are also called constants those of one argument are called unary and those of two binary The result sort appears after gt Use ops when two or more operations of same arguments are declared together and use white spaces to separate them ops plus mult Nat Nat gt Nat There are few special characters in Maude If you use op in the above then only one operation called plus mult is declared 12 The two equations in PEANO NAT are properties or constraints that these operations should satisfy More precisely any correct implementation of Peano natural numbers should satisfy them All equations are quantified universally so we should read for all M and N of sort Nat plus s N M s plus N M All equations in a module can be used
14. t op plus Nat Nat gt Nat Intuitively the reason is that because we want plus to be completely defined in terms of zero and succ Formally this means that any term over the syntax zero succ and plus can be shown using the given equations equal to a term containing only zero and succ operations that is zero and succ alone are sufficient to build any Peano number For that reason they are called constructors 29 Defining Operations using Constructors There is no silver bullet recipe on how to define defined operators but essentially the main safe idea is to Define the operator s behavior on each constructor That is what we did when we defined plus in PEANO NAT and mult in PEANO NAT we first defined them on zero and then on succ In general if c1 cn are the intended constructors of a data type in order to define a new operation d make sure that all equations eq d c1 X1 eq d cn Xn are in the specification This gives no guarantee e g one can define plus as plus succ M N plus succ M N but it is a good enough principle to follow 30 Defining Operations on Lists Let us consider the following specification of lists mod INT LIST is protecting INT sort IntList subsort Int lt IntList op __ Int IntList gt IntList Lid nil op nil gt IntList endm Therefore there are two constructors for lists the empty list and t
15. tegers as isort did above In order to define it define another operation bt insert IntList Tree gt Tree which inserts each integer in the list at its place in the tree and also use the already defined flatten operation
16. tributes are logically equivalent to appropriate equations such as eq A B C A B C eq At B Bt A gt attention rewriting does not terminate eq At O A Then why are the ACI attributes necessary For several reasons 1 Associativity removes the need for useless parentheses Maude gt parse 10 2 3 Int 10 24 3 2 Commutativity will allow rewriting to terminate The normal form will however be modulo commutativity 3 ACI matching is perhaps the most interesting reason It will be described next 22 23 Matching Modulo Attributes Lists occur in many programming languages The following module is a an elegant but tricky specification for lists of integers with a membership operation _in_ mod INT LIST is protecting INT sort IntList subsort Int lt IntList op nil gt IntList op __ IntList IntList gt IntList assoc id nil op _in_ Int IntList gt Bool var I Int vars LL IntList eq I in LIL true eq I in L false owise endm 24 Note the declaration subsort Int lt IntList which says that integers are also lists of integers Then the constant nil and the concatenation operation __ can generate any finite list of integers Maude gt parse 12345 IntList 12345 Maude gt red 1 nil 2 nil 3 nil 4 nil 5 6 7 nil result IntList 1234567 Further by AI matching the membership operation can be defined without having to traverse the list element by ele
Download Pdf Manuals
Related Search