FORMAL SPECIFICATION and
VERIFICATION of SOFTWAREColin D. Walter & Stephen E. Eldridge
Department of Computation
UMIST
PO Box 88
Man hester M60 1QD, UK
www. o.umist.a .uk

1 Importan e of Formal Spe i ation
The normal task of a software ompany is to onstru t programs and systems
from an informal natural language des ription of what they should do, and tomaintain them. Bridging the gap between the natural language des ription andthe programming language ode are s ripts written in more or less formal spe i ation languages (see also arti les "Problem Domain System Analysis" and"Software Life Cy les"). Here we onsider those spe i ation languages thatare formal. Their grammar, or syntax, and their meaning, or semanti s, should
therefore be pre ise and unambiguous.
S ripts in su h languages are not usually exe utable, that is, they do not
say how to do anything. Their aim is to apture exa tly what the user wants
so that the software engineer builds the right produ t, without relying entirely
on a vague requirements des ription from the user. However, they ontain little
or no information as to how the ne essary omputations might be done. This iswhat the programmer adds to obtain the nal ode. There is always an initial
dialogue between the ustomer and software engineer to determine what produ t
is desired. Most of these dis ussions involve making the needs more pre ise.
Spending time on building the wrong produ t an be very ostly espe ially
if prototyping is not possible or the results annot be seen until nal assembly. It is therefore very important, ost-e e tive and time-saving to use formal
spe i ation languages at this early stage to determine all but the most trivial
level of detail for what is required. In reasingly, both onsumer and supplier are
requiring formal spe i ations as part of their ontra t in order to make possible
or defend against laims for damage in litigation.

1.1 Levels of Formality
One signi ant problem with spe i ations is that they appear unfriendly; it an
be diÆ ult to onstru t, read or understand them. This is normally over ome by

2

Con ise En y lopedia of Software Engineering

having a hierar hy of levels of detail and formality, in whi h the initial informal
des ription is moulded into the nal formal spe i ation over several intermediate stages, and de omposed into modules small enough to be fully omprehended.
All those di erent levels are kept together as do umentation for the ode, andwould be read in in reasing order of formality and detail as introdu tion toaid omprehension of the end produ t. Thus, spe i ations are developed like
software using normal engineering te hniques su h as stepwise re nement andtop-down design. Indeed, both spe i ation and software need to be produ ed
simultaneously, the rst do umenting the se ond, for the spe i ation to be of
any pra ti al use in maintenan e or veri ation.

1.2 Levels of Cost
Another apparent problem with writing a formal spe i ation is the ost. Although spe i ation languages are no more ompli ated than programming languages, unfamiliarity with their apparently more abstra t notions makes software engineers relu tant to ta kle spe i ation, and so experts may need to be
used. Veri ation is more diÆ ult, but that is a di erent subje t, requiring the
produ tion of a formal spe i ation rst. There are many short uts avoiding expense. In parti ular, there is often no need to spe ify everything fully: the lowest
level pro edures might not require spe i ations distin t from their ode, andmany variables may not be suÆ iently important to require pre ise de nitions.
Indeed, spe i ation of any part of a pie e of software is perhaps only justi ed
when the produ t is going to be widely or frequently used, has safety- riti alappli ations, malfun tion has severe nan ial impli ations, or ontinuous maintenan e is expe ted, i.e. wherever the need for orre t ode justi es the extra
ost.

2 Basi Terminology
Spe i ation has a number of purposes. In de reasing order of usage this in ludes
onstru tion, maintenan e and veri ation. For ea h of these, the level of spe i ation needed to do ument ode is very similar. Initially one needs pre- andpost- onditions written in predi ate logi . If we all these P and Q respe tively,
and onstru t ode C to meet this spe i ation, then we may write

fP g C fQg
where f g are the omment bra kets for the programming language. This meansthat if the initial data satis es P and C is exe uted su essfully, then the nal
data satis es Q. In this ase we say C satis es the given spe i ation or that it
is partially orre t. There is no laim that the ode will terminate or will doso without raising an ex eption, but if it always does for initial data satisfying
the pre- ondition, then it is said to be totally orre t.

D. Morris & B. Tamm eds, Pergamon Press, 1991, pp 331-338

3

At any point within some ode we an insert a predi ate formula, usually
written within omment bra kets. Thus, the property P between se tions of
ode C and D in

C fP g D
is alled an assertion. It is something that is expe ted to be true of the datawhenever ontrol passes that point during exe ution. Within ertain restri tions,su h as avoiding unbounded quanti ation, it might be possible during run-time
to evaluate P . This an be espe ially valuable when debugging be ause it angive mu h more information than strong typing, and an enable errors to be
dis overed mu h loser to their origin.

3 Programming Language Semanti s
3.1 Assignment
Spe i ations should enable us to write orre t ode, but this is only possible if
we know what the various onstru ts in the programming language are supposed
to do they need spe ifying. Imperative programming is based on what theassignment statement does, namely,fQ(x=t)g x := t fQg(assignment)(The notation of the pre- ondition is explained in the next paragraph.) In termsof manipulating numbers in a ma hine, this ode states that the value of theexpression t is to be assigned to the variable x. However, in terms of the properties of the data held in the ma hine, its spe i ation de lares that in order toobtain property Q for the data immediately after its exe ution we need the data
to satisfy property Q(x=t) immediately before its exe ution.
The pre ise meaning of Q(x=t) in the above axiomati de nition of assignment is not important here. Roughly speaking, it is a slightly altered version of
the formula Q in whi h every so- alled \free" o urren e of x has been repla ed
by t. An o urren e of x is bound if it is in a subformula of Q with the form
8xQ1 or 9xQ1 , where 8 and 9 are the usual quanti ers \for all" and \there
exists". O urren es whi h are not bound by a quanti er are free. However, theformation of Q(x=t) may also involve renaming some bound variables in orderto prevent onfusion between o urren es of variables introdu ed into Q by thesubstitution and those already asso iated to the quanti ers appearing in Q.
The de nition of assignment is an axiom s heme in the proof system we would
use to verify any imperative ode. From it we an dedu e the partial orre tnessof, for example,
fTrueg x := 2 fx = 2g:
This statement laims that any input satisfying the empty ondition True (i.e. norestri tion on the input) will, after exe ution of x := 2, produ e data satisfying
x = 2. This is ertainly what we would expe t the ode to do. To prove it,Con ise En y lopedia of Software Engineering

4

the assignment rule is applied. The pre- ondition whi h yields the desired postondition x = 2 is obtained by repla ing free o urren es of x by 2. This gives
2 = 2, whi h is equivalent to True. So the spe i ed ode fTrueg x := 2 fx = 2g
is partially orre t. A proof of total orre tness is straightforward here be ausethe expression 2 on the right side an ertainly be omputed on any ma hine
without run-time errors or non-termination, and assignment of the result tomemory should not ause problems.

3.2 Veri ation Conditions

The equivalen e of 2 = 2 to True really just needed a proof of the impli ation
True ! 2 = 2. In general, our spe i ation provides a pre- ondition P to theode, but partial veri ation, as above, generates a weakest pre- ondition P 0 . Ine e t P 0 des ribes the widest set of input for whi h the ode will produ e output
with the desired properties. So we are left with a formula P ! P 0 whi h needs

to be proved. Thus, the need to prove pure predi ate formulae arises naturally
in program veri ation, and is the point where theorem provers are required.

3.3 Sequen ing and Bran hing
The other basi omponents of programming languages are sequen ing, bran hing and looping. Ea h is onstru ted from smaller se tions of ode. If these
subse tions are known to satisfy parti ular spe i ations, then a spe i ation
for the whole onstru t an be dedu ed using an inferen e rule. For example,
writing the list of hypotheses above a line, and the onsequen e below, we havethe sequen ing rulefP g C fQg; fQg D fRg
fP g C ; D fRg(sequen ing)

The two hypotheses above the line say we start with the assumptions (i) that if
omputation starts with data satisfying P and exe utes C su essfully then Q
will hold, and (ii) that if omputation starts with data satisfying Q and exe utes
D su essfully then R will hold. Clearly, if we start with data satisfying P , andthen su essively and su essfully exe ute rst C , so that Q holds, and then D,then the output data will satisfy R. This is what is laimed by the on lusion
given below the line.
Bran hing an be de ned axiomati ally in a similar fashion:fP g C fQg; fRg D fQg
f(P &B ) or (R & not B )g if B then C else D fQg(bran hing)

In this ase, the output from exe uting C or D is assumed to be Q, given input data with properties P and R respe tively. The on lusion of the rule isthat (P &B ) or (R & not B ) is the pre- ondition required for the onditional
statement to give output satisfying Q. This formula involves the logi al operators &, or and not whi h are identi al to the Boolean operators found inD. Morris & B. Tamm eds, Pergamon Press, 1991, pp 331-338

5

the programming language itself. The Boolean expression B is, of ourse, a respe table formula of predi ate al ulus. As observed in the assignment example
with True ! 2 = 2 the apparently ompli ated pre- ondition an often be
simpli ed substantially.

3.4 Repetition
Repetition is the most interesting onstru t as far as veri ation is on erned.
Its axiomati spe i ation is this:fP g C fP g
fP g while B do C fP & not B g(looping)

It is really not at all obvious that this rule is the slightest bit helpful! Above
the line, the hypothesis about what C does seems to say very little: exe utionof C does not do anything to the property P of the data. Worse still, the loop
itself seems to do little more: the output data fails to satisfy B , but at least stillsatis es P , as it did before. The key to seeing the usefulness of the rule is that
not B provides information that allows P & not B to release the properties wewant. This is illustrated in the pro edure Add below.
However, the major diÆ ulty of this rule in veri ation is that knowledgeof the formula P & not B does not enable the formula P to be dedu ed. The
problem is that the formula P & not B is not provided synta ti ally separated
onveniently into omponents P and B , but as a semanti ally equivalent formula.
Thus, (P 0 & not B ) & not B is semanti ally equivalent to P 0 & not B , but
synta ti ally we ould extra t either P 0 & not B or P 0 as the formula P . We
annot know what formula to pi k for P without help from the programmer.
The formula P is alled a loop invariant, and in it the programmer needs tostate the umulative properties he intends the loop to have a hieved at the endof a typi al iteration.
Further onstru ts an be spe i ed in a similar manner to obtain the fullaxiomati semanti s of the language. Pro edure and fun tion alls are ompliated by su h things as various parameter passing me hanisms, side e e ts, lazyor eager evaluation, and order of evaluation of expressions and parameters. This
learly requires a deeper treatment than an be given here. For this, the interested reader is referred to [2℄ or [3℄.

4 Programming Example
4.1 Informal Des ription & CodeLet us look at an example in Pas al, starting with a brief semi-formal des riptionof the notation and an idea of the spe i ation. This forms the bridge between theformal spe i ation, whi h is presented by annotating the ode, and an informal
requirements des ription. It should explain both the ode and its spe i ation.

6

Con ise En y lopedia of Software Engineering

The main data stru ture of the program segment given below is Register =Array[Index℄ of Bit. It is used to hold the bits of numbers written in binary notation. So the bit element A[i℄ of the array A : Register is the oeÆ ient of 2i in
axIndexA[i℄2i,the number held in A. Hen e the value of the number in A is M
i=0
whi h will also be written as A.
Part way through the hand al ulation of the sum of two numbers, the sum of
the numbers represented by the rst few digits has been found. The pro edure
Add here mimi s this, and so it is useful to de ne AI to be the value of thenumber in the rst I +1 bits, those with indi es from 0 up to I . So we take AI =Ii
i=0 A[i℄2 . The number represented by taking no bits at all is 0, and so wehave A 1 = 0. In this notation the value of A is AM axIndex sin e the array has amaximum index value of MaxIndex. The largest Register value possible is given
by an array in whi h every bit is 1. If we all this MaxReg , then MaxReg [i℄ = 1
for ea h i : Index. It represents the number MaxReg = 2M axIndex+1 1.
The pro edure below is to output an over ow ondition when the sum of the
inputs is greater than MaxReg and otherwise output the sum In1+In2 of the
inputs. The addition is done bit-wise as in a simple hardware adder or as in a
hand al ulation, with the same de nition of arries. (Here the latter analogy isslightly more appropriate as the bit values are expressed in terms of mathemati al fun tions rather than logi gates.)P

P

Const MaxIndex= 31 ;
Type Index= 0..MaxIndex ;IndexPlus1 = 0..MaxIndex+1 ;Bit= 0..1 ;Register= Array[Index℄ of Bit ;Pro edure Add(In1,In2 : Register ;Var SumOut : Register; Var Overflow : Bit) ;{ Write only: SumOut, Overflow }{ Pre-Add: True }{ Post-Add: (In1+In2  MaxReg $ Overflow = 0$ SumOut = In1+In2 }Var I: IndexPlus1 ;Carry : Bit ;Begin { Add }I:= 0 ;
Carry := 0 ;While I <= MaxIndex do
Begin
SumOut[I℄ := (Carry + In1[I℄ + In2[I℄) mod 2 ;Carry:= (Carry + In1[I℄ + In2[I℄) div 2 ;I:= Su (I)
{ (In1I 1+ In2I 1 = SumOutI 1+ Carry*2I) &(0  I  MaxIndex+1) }End ;Overflow := CarryD. Morris & B. Tamm eds, Pergamon Press, 1991, pp 331-338

7End ; { Add }4.2 The Spe i ation
As in this example, ode should ontain in-line the formal spe i ation. Thisin ludes, rst of all, against ea h type de laration, data invariants whi h areproperties expe ted to hold for all variables of that type. There are no restri tions
for the types used here, but examples of this are given below where we des ribe
some spe i ation languages. Next, pre- and post- onditions for the pro edureneed to be given in the pro edure heading. These are of the kind des ribed at
the beginning of this arti le, and refer to the fun tional properties of the bodyof the pro edure.
Also in the heading there should be information about any use made of variables global to the pro edure. Lists of those variables whose values are a essedor updated must be provided. This enables one to dedu e the following. If P isa property whi h holds before a all to the pro edure and P ontains no freeo urren es of any global variables whi h are updated, then P will still hold after
exe ution of the all. In other words, property P will hold after the pro edure all
if it held beforehand and none of its free variables has had its value hanged. The
onsequen e of in luding these lists is that pre- and post- onditions for pro edures an be made simpler be ause they do not need to in lude su h properties.
Indeed, the post- ondition need only des ribe what hanges have been made tovariables whi h are updated, that is, those in the write lists.
With the detail in the heading xed, the programmer an omplete the ode.
This onstru tion demands that he or she de ides how the addition is to be done,
and, in parti ular, what needs to have been a hieved at the end of ea h iterationof the loop. This is inserted in the ode as an assertion, whi h, in this spe iinstan e is alled a loop invariant and is the property named P whi h we use
when applying the looping inferen e rule above to verify the ode. It ontains
algorithmi information whi h a program veri er annot be expe ted to dedu e.
In the pro edure Add, there is one loop invariant, namely,(In1I 1 + In2I 1 = SumOutI 1 + Carry  2I ) & (0  I  MaxIndex+1)

The loop inferen e rule states that at the end of the loop this property holds
together with not B where B is the Boolean ondition in the loop. Sin e not B
is I > MaxIndex and the loop invariant gives I  MaxIndex+1, it is easy todedu e I = MaxIndex+1. Substituting this value into the loop invariant yields
In1M axIndex + In2M axIndex = SumOutM axIndex + Carry  2M axIndex+1 at theend of the loop, that is,In1 + In2 = SumOut + Carry  2M axIndex+1
This illustrates how the rule for loops really does produ e something useful.
It is the pre- and post- onditions and loop invariants whi h are essential toenable automati program veri ation, for human understanding of the ode, and8Con ise En y lopedia of Software Engineering

for maintenan e purposes. However, the informal spe i ation was also useful,making it easier to understand the formal one whi h do uments the ode, andbeing fairly important to the understanding of the ode.

4.3 Partial Veri ation
A program veri ation tool starts with the post- ondition, applies the inferen e
rules and axioms as above whi h de ne program onstru ts, and makes use ofloop invariants to dedu e the weakest pre- ondition, say Q, whi h the initial
data has to satisfy. This may not mat h the pre- ondition P supplied in thespe i ation. Clearly, to omplete the proof we need P ! Q to hold initially.
This is alled a veri ation ondition, and is a pure predi ate al ulus formula.
We had the example 2 = 2 ! True above. Veri ation onditions arise inparti ular at points where assertions have to be supplied. Consider loops as an
example. To prove the loop against its spe i ation, the veri er must rst prove
the hypothesis in the looping rule and then apply that rule to on lude the loop
is orre t. In proving this hypothesis, the supplied loop invariant P is used as
the post- ondition on the loop body, and the veri er dedu es the weakest preondition Q. This may not oin ide with the pre- ondition, also P , required by
the inferen e rule for loops. In su h a ase, P ! Q would need to be proved inorder to show that input satisfying P will indeed satisfy the pre- ondition Q.

4.4 Termination
Total veri ation of the example above requires a proof that everything terminates properly. Assuming that the range of implemented integers in ludes thevalues of MaxIndex+1 and 3, it is fairly straightforward to he k that everything respe ts the type restri tions, in luding all intermediate al ulations. So
the only possible sour e of improper termination would be if the while loop werein nite. Normally, to prove termination of loops we need to exhibit a fun tion of
the data with ertain properties in respe t of its values at the end of ea h iteration. The fun tion needs to rea h an a eptable value in a nite number of steps.
With real number omputing, this fun tion might be an estimate of error, whi h
we must show tends to zero so that it is eventually small enough. In dis rete
omputing, as here, the fun tion is often a monotoni ally de reasing natural
number valued fun tion. Thus, in the example, the fun tion MaxIndex+1 I
de reases stri tly on ea h iteration, is initially positive, and is always at least
0 (by the type onstraints, whi h ought to have been he ked). As the numberof values that the fun tion an have is at most one more than its initial value,
there are at most that number of iterations of the loop: a nite number. So theode terminates properly.
Further detail about spe i ation of languages and programs and their veriation is to be found in referen es [1℄, [2℄, [3℄ and [6℄.

D. Morris & B. Tamm eds, Pergamon Press, 1991, pp 331-338

9

5 Spe i ation Languages
There is mu h more to veri ation than the total orre tness onsidered so far.
Two spe i ation languages, Z and VDM, provide notation whi h makes easy asystemati treatment of further aspe ts.
Spe i ations of operations in VDM, and in the similar spe i ation method
Z, make use of a state whi h, in terms of Pas al, may be thought of as the set ofvalues of the global variables whi h our operations or pro edures may use. This
is often expressed by saying that VDM and Z are model-oriented approa hes,
meaning that their spe i ations de ne operations by their e e t on externalvariables from a state. This requires
1. de nition of the set of states
2. de nition of the initial state(s)3. spe i ation of implementable operations whose external variables
are parts of the state.
We shall give an example, whi h will also serve to show what kind of notation
is used. It on erns the storage manager of an operating system. The manager
must asso iate ea h available blo k of storage with its user.

5.1 Example in VDM: The Spe i ation
Let B be the set of storage blo ks and U be the set of users. The asso iation of
blo ks with users is spe i ed by a partial fun tion from B to U . The fun tion ispartial be ause some blo ks may not be used. It helps to keep expli it tra k of
the unused, or free, blo ks. Hen e we are led to onsider a state whose externalvariables are the partial fun tion dir : B ! U and the set free  B .
First, we shall show how to make use of this state using the notation of VDM.
The types of the variables in the state are written

dir : map B to U andfree : set of B:
The free blo ks are pre isely those whi h are not in the domain of de nition ofdir. Hen e we have the data invariant:

free = B dom(dir):We ould de ne a re ord, or omposite, type to store this information if we liked.
The VDM notation for su h a type is

SM :: dir : map B to U
free : set of Bor

10

Con ise En y lopedia of Software Engineering

SM 4 ompose SM of
dir : map B to U
free : set of B
end
where ea h value, sm : SM , must satisfy the data invariant
inv SM (sm) 4 free(sm) = B dom(dir(sm)):(The symbol 4 is shorthand for \is de ned by".) The initial state, with noblo ks allo ated, has dir = ; (the empty map) and free = B .
Consider the operation, REQUEST , whi h nds an unused blo k b for a useru (and updates dir and free appropriately). We spe ify it by using a heading,rather like a fun tion head in Pas al, whi h shows the names and types of the
inputs and outputs. We then list the external variables from the state whi h theoperation uses. These are marked rd if they are read only or wr if they may also
be written to or hanged. Finally we write a pre- ondition whi h must be satis edby the inputs and state values before the operation is done and a post- ondition
whi h must be satis ed by the outputs and state variables after the operation isdone. The post- ondition is likely to have to refer to the values of the inputs andvalues of state variable before the operation is done. To distinguish values of statevariables before and after the operation we de orate the previous values with ahook. This de oration is only ne essary in post- onditions sin e pre- onditions
an only refer to initial state values. The spe i ation of REQUEST may be
written in this style as follows.

REQUEST (u : U ) b : B
ext wr dir : map B to U
ext wr free : set of B
pre free 6= ;**post b 2 free ^ free = free fbg*^ dir = dir y fb 7! ug

In this spe i ation we impli itly assume that dir and free satisfy the datainvariant: free = B dom(dir). y is the override operator whi h here gives
pre eden e to the new asso iation of b with u rather than any previous asso iation given by dir. In this ase we ould equally well have used [ but it would
then not have been so lear that our new value for dir is still well-de ned.

5.2 Example in VDM: Proof Obligations
Su h a spe i ation immediately gives rise to a proof obligation. We must provethat the operation is implementable. This does not usually mean writing aomputer program whi h satis es the spe i ation but one should show that,given a state and input satisfying the pre- ondition, there is a state and output

D. Morris & B. Tamm eds, Pergamon Press, 1991, pp 331-338

11

satisfying the post- ondition. In parti ular one must show that the resulting state
does not ontain variables whi h fail to satisfy the appropriate data invariants.
In our example this entails showing that free = B dom(dir) still holds after
the operation REQUEST is performed.
We usually start with an impli it spe i ation whi h is very abstra t anddoes not say how to implement the operation, merely what it should do. Thishas great advantages. Su h a spe i ation is likely to be more on ise than an expli it de nition whi h ontains implementation detail. It also is more adaptable,leaving us free to hange the a tual types and algorithms used in an implementation without having to rewrite our spe i ation from s rat h. Nevertheless weshall have to make our spe i ation more on rete in order to make sure that an
implementation really does satisfy the spe i ation. This pro ess, whi h usually
pro eeds in several steps, is alled data-rei ation. In our example we would
probably not be able to use sets to implement free or fun tions in order to implement dir but might have to use some sort of list and list of pairs respe tively.
We rst de ne a new type for storing information about the storage manager
and then rewrite the spe i ations of our operations, REQUEST et ., to suit
this new type. In order to show that this rei ation step has worked properly
we must dis harge several more proof obligations.
First we must show that our new type ontains at least one representativefor ea h member of our previous storage manager type SM . If we an show thisthan our new type is alled an adequate representation of SM .
Then we must prove various properties of our new operations. First they must
be shown to be implementable. Then we must show that our new operations orrespond to the old ones. A proof of su h a property is alled an implementation
modelling proof.
Without going into detail about what an implementation modelling proof
entails, we should note that it is onsiderably harder if the original type ontains
two di erent elements whi h are not distinguishable by any nite sequen e of its
operations. This undesirable property is alled implementation bias. In our
example SM is unbiased but our new type is likely to be biased sin e there areseveral lists with the same elements as any given set free with more than one
element, and we do not wish to distinguish between them. The absen e of bias
in SM allows us to de ne the orresponden e between the new type and SM bymeans of a fun tion from the new type to SM . This fun tion is alled a retrieve
fun tion. The presen e of a retrieve fun tion makes implementation modelling
proofs simpler and also gives us a simple riterion for adequa y, namely that the
retrieve fun tion should map the new type onto SM .

5.3 The Same Example in Z: The Spe i ation
The spe i ation language Z is a variant of VDM notation. It uses a generalisation of set omprehension notation, fx 2 T jP (x)g, alled the s hema. A s hema
S has form S 4 [de larationsjpredi ate℄ and is usually written verti ally.

Con ise En y lopedia of Software Engineering

12S
de larations
predi ate

Su h a s hema may be used to de ne a omposite type by putting the eldsof the type in the de laration part and the data-invariant in the predi ate part.
Thus our storage manager type SM an be de ned by:S
dir : B ! U
free : IP(B)free = B n dom(dir)The notation used by Z is often more like standard mathemati al notation
than is the notation of VDM. For example the type of dir is written B ! U(sometimes with a line through the arrow to stress that we are using partial
fun tions) instead of map B to U , and the power set of B (i.e. the set of its
subsets) is written IP(B ) instead of set of B .
S hemas are more versatile than the example above suggests; they may be
used not only for de ning omposite types but also for spe ifying operations.
The following de oration onventions are used:

De oration with ! denotes an input to an operation.
De oration with ? denotes an output from an operation.
De oration with 0 denotes a state after variable.
For example, if s is the value before an operation then s0 is the value afterwards.
Both s and s0 must be de lared in a s hema de ning an operation involving s
be ause the predi ate part of the s hema must show how s is hanged by theoperation (even if there is no hange and s = s0 ).
The s hema spe ifying our operation REQUEST is:

D. Morris & B. Tamm eds, Pergamon Press, 1991, pp 331-338

13

REQUEST
dir; dir0 : B ! U
free; free0 : IP(B)b! : Bu? : U
free = B dom(dir) ^free0 = B dom(dir0 ) ^free 6= ; ^b! 2 free ^free0 = free fb!g ^dir0 = dir  fb! ! u?g
Note that the override operator is now written . The predi ate part of thiss hema ould be simpli ed. For example it follows from b! 2 free that free 6= ;.
There is a ri h s hema al ulus for ombining s hemas and making spe i ations look a eptably on ise. For example, a s hema may have other s hemas inits de laration part. The onvention is that if S has s hema T in its de laration
part then we may expand S by merging the de larations of T with those expli itly present in S and anding the predi ate part of T with the expli it predi ate
part of S .
Hen e the following de nitions:

SM 0
dir0 : B ! U
free0 : IP(B)free0 = B dom(dir0 )
and

SM
SM
SM 0
i.e.

14

Con ise En y lopedia of Software EngineeringSMdir; dir0 : B ! U
free; free0 : IP(B)free = B dom(dir) ^free0 = B dom(dir0 )permit the following, more on ise, spe i ation of REQUEST :REQUESTSM
b! : Bu? : U

free 6= ; ^b! 2 free ^free0 = free fb!g ^dir0 = dir  fb! ! u?g
Readers interested in pursuing the spe i ation languages VDM and Z further will nd very readable a ounts in referen es [4℄, [5℄ and [7℄.

Referen es
1. E.W. Dijkstra, C.S. S holten, Predi ate Cal ulus and Program Semanti s, SpringerVerlag, 1990.
2. R. Dowsing, V. Rayward-Smith, C.D. Walter, A First Course in Formal Logi
and its Appli ations in Computer S ien e, Bla kwell S ienti , 1986, ISBN 0-63201308-7.
3. D. Gries, The S ien e of Programming, Springer-Verlag, 1981, ISBN 0-387-90641X.
4. D. C. In e, An Introdu tion to Dis rete Mathemati s and Formal System Spe i ation, Oxford University Press, 1988, ISBN 0-19-859664-2.
5. C.B. Jones, Systemati Software Development using VDM, (2nd Edition) Prenti e/Hall International, 1990, ISBN 0-13-880733-7.
6. A. Kaldewaij, Programming, Prenti e/Hall International, 1990, ISBN 0-13-2041081.
7. M. Spivey, The Z Notation { A Referen e Manual, Prenti e Hall, 1989.