A Big Example: Binary Numbers

Chapter 8: A Big Example: Binary Numbers

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.

8.1. The Beginning: Binary Numbers

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

8.1.1. The Sorts and Operators

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.

8.1.2. The Length Operator

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

8.1.3. The Bits Operator

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)

Last Bit Only.The simplest case is when we are only trying to extract bits 0 to 0: that is, the right-most bit only.
Single Bit Left.This is a sort-of'error handling'case. If we are trying to extract bitsJto 0, and there is only one bit (B) left, we just returnB. Note that ifJ > 0then we are trying to extract bits which'aren't there'and the obvious and easy thing to do is just returnB.
Final Sub String.This is similar to the previous case except that there is more than one bit left, and we know thatJ > 0. We will definitely need the last bitB, so we move it outside thebitsoperator to'keep'it, decrementJand recursively apply thebitsoperator.
Middle Sub String.In this case we are trying to extract a string from the middle, and we know thatI > 0. Hence, we know we do not need the right-most bitB. So we discard it and recursively applybits.

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)

8.1.4. The Not Operator

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

8.1.5. The Normalize Operator

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

8.1.6. The Greater Than Operator

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 .

Base Cases.The first three equations are the base cases, comparing single bits mostly, and should all be obvious. (The first one compares a bit with a bit string, but should still be obviously true: in the worst caseS=0.) The'(0).Bit'business is because we have included theINTmodule, which also has a'>'operator: and Maude cannot tell which one we mean without help (as an experiment, take them out and see what happens - you get a message about'multiple distinct parses').
Leading zeros.Equation (4) simply says that leading zeros can be ignored.
Leading ones.Equation (5) simply says that no single bitBcan be greater than another bit string that begins with a 1.
More Leading ones.Equation (6) is the'inverse'case: any string1 Smust be greater than a single bitB.
Induction step.Equation (7) compares two stringsB SandC T(rememberthatBandCare single bits, andSandTare strings). It normalizes them both, works out their lengths, and asks if one is longer than the other. If so, the longest one must be bigger (after leading zeros have been discarded). If they are the same length, thenB=C=1, and hence we must (recursively) compareSandT. (Note to slightly confuse the issue, the first occurrence of the operator'>'on the right hand side of equation (7) represents'greater than'overInt.)

8.1.7. The Addition, Multiplication and Decrement Operators

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 for fixed 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.

8.1.8. The Prec...Gather Stuff

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.

8.2. Fixed-Length Bit Strings

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.

Not all operators preserve length.The normalize operator can shorten bit strings; and the addition and multiplication operators can lengthen them.
Initial conditions?How can weforceusers to start off with the correct length bit strings initially?
Two's complement arithmetic.Our arithmetic operators so far (addition, multiplication) only deal withunsignednumbers. If we wish to do two's complement arithmetic, then wemusthave fixed-length strings: two's complement simply does not work otherwise.
Not nice.Finally, even if it worked, it is simply'Not Right'!

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.

Horrible syntax.The syntax is just hideous beyond belief - and would make any code very hard to understand.
No defined type structure.This applies to the first suggestion as well. All our operators would simply be defined as taking arguments of sortBits- we would not be able to easily tell which onesreallyoperated on bytes, words etc.
Just does not work.SupposeAand/orBwere actually alreadylessthaneight bits long? Ourbitsoperator will not make them longer. We would need to introduce yet another operator, to dosign extension- making the syntax even worse.

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.

Leading zeros count.Unlike the generic arbitrary lengthBitssort, withByteany leading zerosmustbe included. If they are left out, then the membership axiom will fail to identify bytes correctly. Because this means that you can end up writing quite long bit sequences (especially when words get long), it is convenient to define some constants. (As an example, we have included three constants. You can of course define any others you want.)
Termination.Note we have defined both the addition and subtraction operators in terms of'++'. We must truncate addition results to the correct length usingbits. Notice that if we had called the addition operator overBits'+'instead of'++',then the reduction of additions would not terminate. This is because in reducingA + B = bits(A + B, 7,0), Maude would find thesame equationagain, since bothAandBare bytes. Hencebits(A + B, 7,0)would reduce tobits(bits(A + B,7,0), 7,0)and then tobits(bits(bits(A + B,7,0),7,0), 7,0)and so on forever.

8.2.1. Exercises

Here are some exercises that will make the coursework easier.

Experiment.Try some reductions usingBINARYandBYTES.
Half-Words and Words.Either extendBYTESor write new modules defininghalf-words(16 bits) andwords(32 bits). Include appropriate constants and addition and subtraction operators. Hints: remember you canoverloadoperatornames provided their argument and/or return types are different.
Logical Operators.Extend the operators for bytes, half-words and words with bitwiseandandor. Hints: it is only necessary to define both operators overBits: they will work properly over bytes and so on (why is this?). To defineand/oroverBits, you will minimally need three equations (two base cases for one-bit words, and one for longer strings); to getand/orto work when used on words of different lengths, you will need one more equation (whenanding/oringa 1-bit word with a longer bit-string). You may wonder what the point ofanding/oringdifferent length strings is: to tell the truth, this is not going to be necessary. However, remember that theBINARYmodule does deal with variable length strings, so for completeness yourand/oroperators should work in such circumstances.
Shift Operators.Defineleft shift,logical right shiftandarithmetic right shiftoperators. These should take two argumentsIandJ, and should shiftIbyJplaces in the appropriate direction, whenJis regarded as anunsignednumber. Hints: it will help to use the'--'operator; once again if shift operators are defined overBits, they should work over bytes etc. In case you are wondering what the difference between arithmetic and logical right shift is: logical right shift always inserts zeros as the new most significant bits of the shifted number, but arithmetic right shift doessign extension(youmight need to remind yourself what that is). An alternative way of thinking about it is: left shift is equivalent to the Java'<<'operator; arithmetic right shift to the Java'>>'operator; and logical right shift to the Java'>>>'operator - which should be explained in Java textbooks. You will probably have to use thenormalizeoperator a lot to get shifting to work.
Conversion Operators.Define yourself some operators that convert between bytes, half-words and words. You might usefully include operators to map bytes to half-words, and half-words to words, each with two versions: one forunsigned, orlogicalvalues which just pads with zeros; and one forsignedvalues that pads with zeros or ones as appropriate. You could also define operators whichextractbytesand half-words from words, and half-words from words; and ones whichassemblebytes into half-words and words, and half-words into words. Your extraction and assembly operators can either beBig EndianorLittle Endian(remind yourself what these are): it does not matter provided you areconsistent.That is, if you assemble, say, four bytes into a word and then extract them out, you should get the same bytesin the same order.
Multiplication.Define multiplication over bytes, half-words and words. Hint: this is slightly less straightforward than addition and subtraction because multiplication does not'work'over two's complement numbers in the same way that addition/subtraction do. You must first make sure that the numbers to be multiplied are both converted (if necessary) topositivenumbers, and the result is converted, if necessary back to negative. Sub-hint: remember that you can tell if a two's complement number is negative or positive by looking at the most significant bit. Yet another hint: remember you will need to define multiplication in terms of the'**'operator. If you are feelingreallykeen, you could replace the current equations defining multiplication inBINARYwith ones definingBooth's Algorithm, whichdoeswork with two's complement numbers.

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!

8.3. Aside: A Trap for the Unwary

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.

Previous Contents Next