In this chapter we are going to look at a fairly large example - based on a set of Maude modules - that allow us to represent and manipulate binary numbers. This example is partly chosen because it contains examples of everything we have seen so far, but mostly because it will beveryuseful in the main coursework.
The first moduleBINARYis a (slightly edited) version of a module that is provided with Maude as an example. Just for completeness, here is the entire module. We will repeat appropriate parts of this below. You are very strongly encouraged to experiment with this module - you will be using it extensively in your coursework.
fmod BINARY is protecting INT . sorts Bit Bits . subsort Bit < Bits . ops 0 1 : -> Bit . op __ : Bits Bits -> Bits [assoc prec 1 gather (e E)] . op |_| : Bits -> Int . op normalize : Bits -> Bits . op bits : Bits Int Int -> Bits . op _++_ : Bits Bits -> Bits [assoc comm prec 5 gather (E e)] . op _**_ : Bits Bits -> Bits [assoc comm prec 4 gather (E e)] . op _>_ : Bits Bits -> Bool [prec 6 gather (E E)] . op not_ : Bits -> Bits [prec 2 gather (E)] . op _-- : Bits -> Bits [prec 2 gather (E)] . vars S T : Bits . vars B C : Bit . var L : Bool . vars I J : Int . *** Length eq | B | = 1 . eq | S B | = | S | + 1 . *** Extract Bits... eq bits(S B,0,0) = B . eq bits(B,J,0) = B . ceq bits(S B,J,0) = bits(S, J - 1,0) B if J > 0 . ceq bits(S B,J,I) = bits(S,J - 1,I - 1) if I > 0 and J > 0 . *** Not eq not (S T) = (not S) (not T) . eq not 0 = 1 . eq not 1 = 0 . *** Normalize supresses zeros at the *** left of a binary number eq normalize(0) = 0 . eq normalize(1) = 1 . eq normalize(0 S) = normalize(S) . eq normalize(1 S) = 1 S . *** Greater than eq 0 > S = false . eq 1 > (0).Bit = true . eq 1 > (1).Bit = false . eq B > (0 S) = B > S . eq B > (1 S) = false . eq (1 S) > B = true . eq (B S) > (C T) = if | normalize(B S) | > | normalize(C T) | then true else if | normalize(B S) | < | normalize(C T) | then false else (S > T) fi fi . *** Binary addition eq 0 ++ S = S . eq 1 ++ 1 = 1 0 . eq 1 ++ (T 0) = T 1 . eq 1 ++ (T 1) = (T ++ 1) 0 . eq (S B) ++ (T 0) = (S ++ T) B . eq (S 1) ++ (T 1) = (S ++ T ++ 1) 0 . *** Binary multiplication eq 0 ** T = 0 . eq 1 ** T = T . eq (S B) ** T = ((S ** T) 0) ++ (B ** T) . *** Decrement eq 0 -- = 0 . eq 1 -- = 0 . eq (S 1) -- = normalize(S 0) . ceq (S 0) -- = normalize(S --) 1 if normalize(S) =/= 0 . ceq (S 0) -- = 0 if normalize(S) == 0 . endfm
protecting INT . sorts Bit Bits . subsort Bit < Bits . ops 0 1 : -> Bit . op __ : Bits Bits -> Bits [assoc prec 1 gather (e E)] . op |_| : Bits -> Int . op normalize : Bits -> Bits . op bits : Bits Int Int -> Bits . op _++_ : Bits Bits -> Bits [assoc comm prec 5 gather (E e)] . op _**_ : Bits Bits -> Bits [assoc comm prec 4 gather (E e)] . op _>_ : Bits Bits -> Bool [prec 6 gather (E E)] . op not_ : Bits -> Bits [prec 2 gather (E)] . op _-- : Bits -> Bits [prec 2 gather (E)] .
We introduce two sortsBit(meant to represent asingle bit) andBits(meant to representone or morebits in a string). Notice, quite naturally, we makeBita subsort ofBits.
We then introduce a range of operators - for now, ignore the'prec gather'stuff: we will briefly explain thatbelow.The first operator is the most important and conceptually difficult. The operator'__'(two underscores) is thebit string concatenation operator. Recall that we use underscore to indicate in an operator name that we are using mixfix and that underscores are replaced by arguments. Because this operator only has underscores in its name, to concatenate a pair of bit strings we simplywrite them next to each other(with a space). That is:
1 0
is the bit string'10'- consisting of 1 concatenated with 0. And:
1 1 0 0 1
is the bit string'11001'consisting of 1 concatenated with 1, then with 0, then with 0, and then with 1. Because this operator is associative
(1 (1 (0 (0 1)))) = ((((1 1) 0) 0) 1)
and so on - so we do not need to include any brackets (actually we also need the'prec gather'stuff for that as well - seebelow).
The next operator is thelengthoperator - it returns the length of a bit string as anInt. Thenormalizeoperator deletes leading zeros from bit strings. Why do we need this? TheBINARYmodule deals with bit strings ofarbitrarylength, and typically we would regard, say:
0 0 0 1 1 0 0 1 = 1 1 0 0 1.
But Maude willnotregard these as equal. Hence it is usual to apply thenormalizeoperator first, to delete leading zeros, before comparing numbers (and in some other cases as well).
Thebitsoperator is used to extractsubstringsfrom binary strings - you will use this in the course work to both'chop up'strings and totruncatestrings.We have included'--'which is thedecrement operator. This is a slightly strange thing to include (and we will talk a bit more about thatbelow) but you will find it useful to defineshift operators.
All the other operations have the usual meanings - but note that we have used'++'and'**'for multiplication and addition - all will be explainedlater.
We will not go through the variable declarations - they are fairly obvious - except to say that in the following sections,SandTalways represent variables of sortBits;BandCof sortBit;Lof sortBool; andIandJof sortInt.
The length operator is recursively defined by two equations.
eq | B | = 1 . eq | S B | = | S | + 1 .
That is, the length of a single bit is 1, and the length of a bit stringSfollowed by a single bit is 1 plus the length ofS(we use'+'and not'++'because we are addingInts). For example:
| 1 1 0 | = | 1 1 | + 1 = | 1 | + 1 + 1 = 1 + 1 + 1 = 3
This is quite a complex operator:bits(S,J,I), whereJ > I, extracts the substring consisting of bitsJtoIfrom stringS. Thebitsoperatorassumes that all bits in a string arenumberedfromrighttoleft:
bit numbers: 8 7 6 5 4 3 2 1 0 example: 1 0 1 1 0 0 0 1 0
Here are the equations (with numbers added). There are four cases to consider.
eq bits(S B,0,0) = B . (1) eq bits(B,J,0) = B . (2) ceq bits(S B,J,0) = bits(S, J - 1,0) B if J > 0 . (3) ceq bits(S B,J,I) = bits(S,J - 1,I - 1) if I > 0 and J > 0 . (4)
Here is an example of bits in operation:
bits(1 1 0 0 1 0 0 1, 5, 2) *** Should be 0 0 1 0 = bits(1 1 0 0 1 0 0, 4, 1) *** using (4) = bits(1 1 0 0 1 0, 3, 0) *** using (4) = bits(1 1 0 0 1, 2, 0) 0 *** using (3) = bits(1 1 0 0, 1, 0) 1 0 *** using (3) = bits(1 1 0, 0, 0) 0 1 0 *** using (3) = 0 0 1 0 *** using (1)
Thenotoperator just inverts every bit in a string. Here are the equations.
eq not (S T) = (not S) (not T) . eq not 0 = 1 . eq not 1 = 0 .
It works by (arbitrarily) chopping a string into two parts, recursively inverting the two halves, and concatenating them back together. For example:
not(1 0 1 0) = (not(1 0) not(1 0)) = (not(1) not(0) not(1) not(0)) = 0 1 0 1
Note the way we have divided up1 0 1 0is arbitrary - any way works:
not(1 0 1 0) = (not(1) not(0 1 0)) = (not(1) not(0) not(1 0)) = (not(1) not(0) not(1) not(0)) = 0 1 0 1
The normalize operator simply deletes leading zeros. Here are the equations.
eq normalize(0) = 0 . eq normalize(1) = 1 . eq normalize(0 S) = normalize(S) . eq normalize(1 S) = 1 S .
Hopefully, you are beginning to get the hang of this - so here is an example with no further explanation.
normalize(0 0 0 1 0 1) = normalize(0 0 1 0 1) *** since normalize(0 S) = normalize(S) = normalize(0 1 0 1) *** --- ditto --- = normalize(1 0 1) *** --- ditto --- = 1 0 1 *** since normalize(1 S) = 1 S
This one is the most complicated so far - it is made more so because it deals with arbitrary length strings, and so we could be comparing strings of unequal length. Here are the equations, again with numbers.
eq 0 > S = false . (1) eq 1 > (0).Bit = true . (2) eq 1 > (1).Bit = false . (3) eq B > (0 S) = B > S . (4) eq B > (1 S) = false . (5) eq (1 S) > B = true . (6) eq (B S) > (C T) (7) = if | normalize(B S) | > | normalize(C T) | then true else if | normalize(B S) | < | normalize(C T) | then false else (S > T) fi fi .
Hopefully, you arereallygetting the hang of this by now. All these operators are defined using equations that simply codify the usual rules of binary arithmetic, with which you are familar. As an exercise, read and ensure you understand the equations - feel free to come and explain your understanding to me, to confirm that you are correct. (As an incentive, I definitely donotguarantee that this will not be an exam question.)
One point deserves mention. When we deal, as in this case, with arithmetic over arbitrary and variable length binary strings, we are essentially talking aboutunsignedarithmetic. For example, suppose we compute some arithmetic result:11. Does this represent a two-bit negative number, representing -1 decimal; or have we just appliednormalizeto delete leading zeros, meaning it is really 3 decimal? In fact, except when it is applied to zero,normalizecanonlyreturn negative numbers - if we we claim to be using two's complement. Consequently, it is easier all round if we just assume that binary numbers in theBINARYmodule are all positive; and we wait forfixed lengthstringsfor negative numbers and subtraction. Despite this, wehaveincluded a decrement operator - which you will find helpful in definingshiftoperations. Notice though that we have included an equation to ensure that it does not count below zero: that is,0 -- = 0.
I promised a brief explanation of the'prec...gather'notation - so here it is. If we don't includeprec 1 gather (e E)(in the specific case of the concatenation operator) and try the following addition (recall that we have called addition over bit strings'++'):
maude>red 1 0 ++ 1 0 . result Bits: 1 1 0
That is,2 ++ 2 = 6, and not the expected result of1 0 0. This is because the default parse is
1 (0 ++ 1) 0
and0 ++ 1 = 1. We could of course bracket the term to force the parse we want, but if we useprec 1 gather (e E)we don't have to (and we would sometimes forget).
The same fundamental concerns apply to the operatorsnot_,_>_,_++_and_**_(all the infix ones). The number after the'prec'denotes the precedence of the operator, and lower numbers mean higher precedence: so concatenation is the highest, followed by not, multiplication, addition, and then greater than - which is, I hope, what you would naturally expect. The term'gather (e E)'tells Maude how to group terms likeA ++ B ++ C: should it be(A ++ B) ++ CorA ++ (B ++ C)?Thegatherterms says it should be the second one. In the case of addition it does not matter, but there are cases where it does.
The example we have just seen deals with arbitrary length strings of bits - this is useful, but we will commonly wish (in the coursework for instance) to deal withfixed lengthstrings - probably withseveral differentsizes of fixed length strings of bits. Typically, these will be 8-bit bytes, 16-bit half-words, 32-bit words, and so on. At first sight, there is no real problem. If we'start off'with strings of a certain length, is this not sufficient? For example, if we wish to deal with bytes, then
not(1 0 1 0 0 1 1 0) = 0 1 0 1 1 0 0 1 .
That is, we started with eight bits and we still have eight bits. There are a few problems with this.
A first alternative is to use thebitsoperator totruncateall bit strings to the correct length. For example, suppose we wish to add two stringsAandB, which are supposedly bytes. We could do this:
bits((bits(A,7,0) ++ bits(B,7,0),7,0).
That is, truncate bothAandBto eight bits, and then truncate the result as well. We do not like this either.
Fortunately, there is a solution of course - we will use sub sorts and membership axioms.Hereis a module defining some operations over bytes.
*** Note to get this to work you must first *** read binary.maude into Maude (or cut and *** paste binary.maude into this file before *** BYTES) *** fmod BYTES is protecting BINARY . sort Byte . subsort Byte < Bits . ops 0-byte 1-byte -1-byte : Byte . op _+_ : Byte Byte -> Byte [assoc comm] . op _-_ : Byte Byte -> Byte . vars b0 b1 b2 b3 : Bit . vars b4 b5 b6 b7 : Bit . vars A B : Byte . mb (b0 b1 b2 b3 b4 b5 b6 b7) : Byte . eq 0-byte = (0 0 0 0 0 0 0 0) . eq 1-byte = (0 0 0 0 0 0 0 1) . eq -1-byte = (1 1 1 1 1 1 1 1) . eq A + B = bits(A ++ B, 7, 0) . eq A - B = bits(A ++ (not B ++ 1), 7, 0) . endfm *** 1 - 2 = -1 red 1-byte - (0 0 0 0 0 0 1 0) . *** -1 + 1 = 0 red -1-byte + 1-byte .
Our new sortByteis a subsort ofBits, and we have introduced a membership axiom:
mb (b0 b1 b2 b3 b4 b5 b6 b7) : Byte .
This says that any sequence of eight bits is a byte. We have defined two operators (addition and subtraction) and three constants: 0, 1 and -1. Two points need consideration.
Here are some exercises that will make the coursework easier.
If you do these exercises, you will have a very useful'tool kit'of modules and operators for handling much of the low level parts of the coursework, and you will have gained useful Maude experience as well.If you cannot get them to work after a serious attempt, then come and ask me!
You may well think that the membership axioms above are clumsy - especially for words. A fairly obvious alternative for bytes and words is
var Y : Bits . cmb Y : Byte if | Y | == 8 . cmb Y : Byte if | Y | == 32 .
where|_| : Bits -> Intis the length operator. The trouble with this is the way Maude deals with [conditional] membership axioms. In alater chapteris an example, which uses the first form of non-conditional axiom, but which contains the conditional form commented out. Try using the conditional form first. While you are waiting for it to finish, read the paragraph below (Hint: I'd typectrl-Cnow:I tried this as an experiment on a 2.4GHz P4 with 1GByte of memory and gave up after 10 minutes CPU time.)
Maude will continually try to apply any membership axioms to narrow a sort to one of its subsorts: in this case,Bitsto one ofByteorWord. It does in the usual way: by pattern matching. In the non-conditional case, only 8-bit and 32-bit words match, and all others get left alone. In the conditional case,everyoccurence ofBitsis a potential candidate, which needs to have its length checked with|_|(which is recursively defined, and takes more rewrites for longer bit strings). This is an additional overhead, made worse because there are likely to be many more occurences ofBitsthan you may first think. Consider the string0 0 0 0 0 0 0 0representing a Byte constant zero. This is not one occurence, but seven because the string is built by successive concatenation of bits using the__operator.So first we construct0 0, which is checked against all the membership axioms, and then0 0 0and so on. If you really want to do some comparisions of the number of rewrites, I suggest you modify the example in theexample chapterto reduce something simple likepc(Mp,Md,Pc,Rg)(i.e. just extract the program counter value from the state). This takes 2 rewrites with the non-conditional axioms, and 720 000 (!) with the conditional ones.