In this chapter, we will look at some very simple 'software' examples in Maude: 'software' because we will look at simple data types for the most part. In the next chapter, we will consider some simple hardware-based examples.
The stack is a 'traditional' example. Here is one in Maude:
fmod STACK is sorts Stack Elt . op EmptyStack : -> Stack . op ErrorElt : -> Elt . op push : Stack Elt -> Stack . op pop : Stack -> Stack . op top : Stack -> Elt . op isEmpty : Stack -> Bool . var S : Stack . var E : Elt . *** Just used in the reductions vars A B : Elt . eq isEmpty(EmptyStack) = true . eq isEmpty(push(S,E)) = false . eq top(EmptyStack) = ErrorElt . eq top(push(S,E)) = E . eq pop(EmptyStack) = EmptyStack . eq pop(push(S,E)) = S . endfm *** top of the empty stack red top(EmptyStack) . *** pop the empty stack red pop(EmptyStack) . *** push A then B on stack, what is *** on top? red top(push(push(S,A),B)) . *** push A then B on stack, then pop *** stack: what is contents of stack? red pop(push(push(S,A),B)) . *** push A then B, then pop stack, *** what is on top? red top(pop(push(push(S,A),B))) .
The main issue with stacks is: what happens when you pop the empty stack? Generally, this is considered to be some form of error: we have slightly ducked the issue by simply making pop(EmptyStack)=EmptyStack. However, we still have the [related] problem of: what is the top of the empty stack? We have introduced a special error element for this. Incidentally, properly handling stacks - especially errors in stacks - is difficult, and was incorrectly handled for many years in the literature. The problem was definitely solved by Professor John Tucker and Professor Jan Bergstra (a regular visitor to Swansea).
We will go through this example quite carefully.
While for many of you the structure of the equations in STACK will be 'obvious', you may still have trouble writing your own. Often when they first try to consider an example like a stack, new users of Maude will try to write something like 'eq pop(S) = ...' - and then not know what to write because they have no idea what (if anything) is in stack S. Notice we solve this problem in the actual equations we write by pushing something on stack S first - so we know what is there.
A key observation when dealing with equations for examples like stacks is that there are three kinds of operator.
Notice in the case of the stack, all of the equations involve applying the dismantling and querying operators to either the 'base case' (the empty stack), or to the result of the building operation (i.e. push(S,E)). That is, equations usually 'make something' and they either 'break it' or 'look at it'. This insight was very useful for me - and hopefully it will help you to be able to write correct equations.
The second issue here is the nature of variables. Variables in Maude are like mathematical variables - you cannot change them. The same is true in logic and functional programming, so you should be used to this idea: except that variables in procedural and object-oriented programming can be changed, so you might forget. It is essential you remember this - failing to do so is a very common reason for mis-writing equations (usually very badly). To make it explictly clear, if a variable S representing, say, a stack appears in an equation, then everywhere it appears in that particular equation it has the same value. You cannot change the stack it represents - you can only make a new stack, that is a [possibly-modified] copy of S. So the operator push : Stack Elt -> Stack takes a stack, and an element: push(S,E) makes a new stack (which it returns as its result) - it does not 'change' the stack S. Hence when we pop the resulting stack we get the old stack (S) back.
pop(push(S,E)) = S
Stacks of some unspecified sort 'Elt' are not very helpful - can we make stacks of other things? Yes - here is part of an example of a stack of natural numbers.
fmod STACK is protecting BASIC-NAT . sort Stack . op EmptyStack : -> Stack . op ErrorElt : -> Nat . op push : Stack Nat -> Stack . op pop : Stack -> Stack . op top : Stack -> Nat . op isEmpty : Stack -> Bool .
We have imported the module BASIC-NAT, and used the sort Nat that it defines instead of Elt. The remainder of the module is essentially identical to STACK (with Elt replaced by Nat). The complete example (including BASIC-NAT) can be found here.
Although this is essentially as much as many programming languages provide (including, say, standard Pascal), it is not ideal: if we want stacks of, say, Reals, or even other stacks, we would have to define another stack module. In fact, we would need one for each kind of stack we want. Is there any way to define a generic stack, in the way that is effectively possible in object oriented languages? (Called generics in Java and C#, and templates in C++.) The answer is yes: however, it is technically quite advanced, and we will not be doing it.
Another, simpler, example is a tuple of data items - an ordered collection much like a record (or structure in C). This is an example of a TRIPLE - which might represent, say, 3D coordinates.
fmod TRIPLE is protecting INT . sort Triple . op _,_,_ : Int Int Int -> Triple . ops Pi1 Pi2 Pi3 : Triple -> Int . vars A B C : Int . eq Pi1(A,B,C) = A . eq Pi2(A,B,C) = B . eq Pi3(A,B,C) = C . endfm
The operator _,_,_ builds a triple from three Ints. The sort Int is defined in the module INT, which is supplied with Maude but not imported by default. It provides a link to the underlying integer arithmetic of the host machine. This is handy because it is efficient and fast. (Incidentally, the functions Pi1, Pi2 and Pi3 are called projection functions, and 'Pi' is the 'traditional' name. Note that our insight into the structure of equations applies here as well: first apply the 'building' operator _,_,_, then the 'query' operators Pi1, Pi2 and Pi3.
The same structure essentially applies to records and structures - TIME is just a re-written version of TRIPLE with different syntax, and an explicit interpretation (namely a time of day).
fmod TIME is sorts Time Hour Min Sec . op _:_:_ : Hour Min Sec -> Time . op _.hour : Time -> Hour . op _.min : Time -> Min . op _.sec : Time -> Sec . var H : Hour . var M : Min . var S : Sec . eq (H : M : S).hour = H . eq (H : M : S).min = M . eq (H : M : S).sec = S . endfm
If you look carefully, you can see a 'syntactic irregularity' when you compare TRIPLE and TIME. In the defining equations, we have put spaces around the ':'s but we did not have to do so with the corresponding ','s in TRIPLE. The spaces are necessary - try taking them out. This is because some characters - brackets, commas - are 'special' and the usual whitespace rules do not apply. Until you get the hang of this, such issues are likely to be the source of syntax errors and general irritation. Similarly, notice that we have bracketed the 'H : M : S terms in the equations. This is because of the default precedence of the _:_:_ and _.hour etc. operators. If the brackets are left out, then the code does not parse correctly (try it). We can change the precedence, but for us the extra complexities involved are not worth it here: however, in the next chapter we will do this to make some terms more 'natural'.
If we are going to have an example of records, we should have one of arrays as well. Both records (or strictly tuples) and arrays (in the form or memories) will be useful for the coursework.
fmod ARRAY is sorts Array Index Data . op _[_] : Array Index -> Data . op _[_/_] : Array Data Index -> Array . var A : Array . vars I J : Index . var D : Data . *** For reductions only vars I1 I2 I3 : Index . vars D1 D2 : Data . eq A[D / I][I] = D . ceq A[D / I][J] = A[J] if I =/= J . endfm *** Change element I1 to value D1, and *** change element I2 to value D2, then *** look up I1 - it should be D1 red A[D1 / I1][D2 / I2][I1] . *** Make the same changes and then look *** up I2 - it should be D2 red A[D1 / I1][D2 / I2][I2] . *** Same changes, but look up I3 (not *** changed) - it should be A[I3] red A[D1 / I1][D2 / I2][I3] .
Once again, we will go through this example.
The second equation in the array example is irritating:
ceq A[D / I][J] = A[J] if I =/= J .
We have to make it a conditional because if we do not, Maude might apply it when I == J and we want the first equation eq A[D / I][I] = D to be used then. In Maude 1, we had no choice about this but Maude 2 has introduced the concept of 'otherwise': you can mark an equation only to be applied if no others can be applied. We can do this for the second array equation like this:
eq A[D / I][J] = A[J] [owise] .
This is generally better in my opinion: it certainly makes the array example in Maude look much more like the mathematical version. I will use [owise] quite a lot, but this is largely a matter of personal taste: you never have to use it. For completeness, here is the new version of array in full.
fmod ARRAY is sorts Array Index Data . op _[_] : Array Index -> Data . op _[_/_] : Array Data Index -> Array . var A : Array . vars I J : Index . var D : Data . *** For reductions only vars I1 I2 I3 : Index . vars D1 D2 : Data . eq A[D / I][I] = D . eq A[D / I][J] = A[J] [owise] . endfm
The final example in this chapter is a binary tree - we will not explain this example in detail as the general structure should be clear by now.
fmod BIN-TREE is sorts BinTree Elt . op null : -> BinTree . op getData : BinTree -> Elt . ops rightTree leftTree : BinTree -> BinTree . op isLeaf : BinTree -> Bool . op makeTree : BinTree Elt BinTree -> BinTree . *** Next operator is justt makeTree with different syntax op [_<-_->_] : BinTree Elt BinTree -> BinTree . vars L R : BinTree . var D : Elt . *** For reductions only vars D1 D2 D3 D4 D5 : Elt . ceq isLeaf([L <- D -> R]) = true if (L == null) and (R == null) . eq rightTree([L <- D -> R]) = R . eq leftTree([L <- D -> R]) = L . eq getData([L <- D -> R]) = D . eq makeTree(L,D,R) = [L <- D -> R] . endfm *** Make a binary tree that looks like this: *** *** D1 *** | *** D2------ D4 *** | *** D5 ------D3 *** *** And navigate from the root D1 to D3 *** (leftTree to D2, then rightTree to D3, *** then getData) red getData(rightTree(leftTree( *** The next line is D2 (left) subtree [[[null <- D5 -> null] <- D2 -> [null <- D3 -> null]] *** The next line is the root of the tree <- D1 -> *** The next line is D4 (right) subtree [null <- D4 -> null]]))) .