Simple Software Examples

# Chapter 5: Simple Software Examples

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.

## 5.1. A Stack

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.

• Sorts: stacks and elements. We have introduced two new sorts - one representing stacks and the other elements stored on the stack (Elt). You may wonder: can we have stacks of other sorts, external to the actual stack module (say, integers). The answer is yes, and we will get back to that later.
• Constants. We have introduced two constants - EmptyStack, representing (obviously) an empty stack; and ErrorElt, representing an error state.
• Operations. There are four stack operators, and they are all 'traditional'. Two (push and pop) operate on stacks (and in object oriented-speak are commands, and two (top and isEmpty) report on the state of stacks (and in object oriented-speak are queries). Incidentally, it is (or was) common to combine the roles of top and pop: this is generally bad practice, because it is necessary to use side effects to update the stack, and is best avoided.
• Variables. We only need two variables S and E to define the required equations: but we introduce two others simply to be used in the reductions.
• Equations. Our first two equations define the behaviour of isEmpty. Clearly, EmptyStack is an empty stack; however if we push an element E on some stack S then the result is a non-empty stack. The next two equations define the behaviour of top and push. Taking the top of an empty stack is an error. If we push an element E on some stack S, then E will be the top element of that stack. The final two equations define the behaviour of pop and push. If we push an element E on some stack S, then pop the resulting stack, we get the [original] stack S back.
• Reductions. We have included some sample reductions. Notice you can include these in files and they are present in the code for STACK. You are strongly encouraged to download these examples and experiment with them. (Maude is a programming language and cannot be effectively learned without practice.)

### 5.1.1. Some Insight into Equations and Variables

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.

• Building operations. Some operators build things - in the case of the stack, the push operator falls into this category.
• Dismantling operations. Some operators dismantle things - in the case of the stack, the pop operator falls into this category.
• Querying operations. Some operators query things - in the case of the stack, the top and isEmpty operators fall into this category.

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

```

### 5.1.2. Stacks of Other Things

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.

## 5.2. Tuples (and Records)

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'.

## 5.3. Arrays

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.

• Sorts. We have defined three sorts - the array sort, the array index sort, and the array data sort. In practice, the last two will probably be imported from elsewhere.
• Lookup operator. The operator _[_] is the array lookup operator. It has the 'usual' programming language syntax: that is, A[I] is element I of array A.
• Update operator. The operator _[_/_] updates an array. More correctly, it makes a new updated copy. The syntax is A[D / I], which makes a new array which is identical to A except that the element at I is replaced by D.
• Equations. The first equation says: make a copy of A with element I changed to D; if we then look up element I we should get D. The second equation says that if we make the same changes but lookup a different element J, we should get whatever was originally in A at location J.
• Reductions. The example reductions show how to make two successive changes to an array A. (This is an important hint for the coursework.)

### 5.3.1. A Better Array

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

```

## 5.4. Binary Trees

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]]))) .

```