FORMAL METHODS IN SOFTWAREENGINEERING
Colin D. Walter
Department of Computation
UMIST
PO Box 88
Man hester M60 1QD, UK
www. o.umist.a .uk

1 Introdu tion
Formal methods in software engineering refers to the use of mathemati s toprodu e more reliable software, and, if ne essary, to prove its orre tness. Itis dis rete mathemati s, and in parti ular mathemati al logi [2℄, [7℄, whi h ismainly used. As in traditional engineering subje ts where it is analogous toontinuous mathemati s, its use is both in the theoreti al foundations of thesubje t, and appli ations.

2 De ning Semanti s
On the theoreti al side, mathemati s is used to make quite pre ise the meaningof programming languages [4℄, [9℄. This is alled axiomati semanti s, operational semanti s, denotational semanti s, operational semanti s, et ., dependingon the view taken. It should in lude a des ription of the model of omputation
expe ted on the target ma hine and a formal treatment of ex eption handling,
as knowledge of both of these is ne essary to enable anything to be proved aboutprograms.

3 Computability & EÆ ien yAt a deeper level, logi also treats problems of omputability through, for example, the study of simple but powerful models of ma hines, su h as Turing
ma hines [5℄. There are tasks that we would like to be able to do using a omputer program, but annot. Of parti ular interest here is the impossibility of
onstru ting a general purpose theorem prover. More generally, the spa e andtime eÆ ien y of algorithms is studied [5℄ be ause only nite resour es are available for omputing. Part of program veri ation involves he king that suÆ ientresour es are indeed provided.

2Con ise En y lopedia of Software Engineering

4 Fun tional Spe i ation
A number of aspe ts are involved in produ ing reliable software but most frequently the fun tional properties are investigated rst. This requires the use ofa spe i ation language to des ribe (i) properties required of the input, alled apre- ondition, and (ii) relationships required between input and output, alled apost- ondition. Su h a pair of formulae is alled a fun tional spe i ation. Codean be written and maintained mu h more su essfully against su h spe i ations than with informal des riptions. Su h methods should be used as widely
as possible, espe ially on riti al omponents of software.

5 Veri ation
In se tions where reliability is paramount, the formally de ned semanti s of the
programming language are then used to prove the software. This requires establishing that if the input satis es the pre- ondition properties (i) then, provided
proper termination o urs, output satisfying the post- ondition properties (ii)is obtained. This stage is alled partial veri ation. Of ourse, when this an
be done, it only establishes that the software is partially orre t with respe t
to the formal fun tional spe i ation. Some problems still remain. First, proper
termination needs to be he ked. But in addition there is no guarantee thatthe spe i ation itself is orre t; higher level des riptions use natural languages,
with all their inherent impre ision and ambiguity, so that onne tions with theinformal requirements annot be given exa tly, let alone proved.
Normally not all of the software needs to be written or maintained rigorously
against a formal spe i ation, and few aspe ts of the software need to be proved
formally in the above way. So usually the formal fun tional spe i ation whi h
is to be onstru ted need only re e t part of the total fun tionality.

6 Spe i ation Languages
A variety of di erent spe i ation languages has arisen be ause of di ering needs
and situations. The raw ingredients of pre- and post- onditions, whi h are written in notation similar to that of standard mathemati al logi , need to be ombined with further information, su h as lists of external variables whose values
may be a essed or updated, or both, in order to make the interfa e with the restof the world omplete and pre ise. For imperative programming languages, thetwo most widely used notations are those of VDM [6℄ and Z [8℄, [11℄. For de larative languages (fun tional and logi programming languages) program s ripts
are mu h loser to the spe i ations we would like to write, and the appropriate
spe i ation language is obtained by doing little more than adding quanti ation to the programming language. (This is equivalent to allowing in nite loops,
whi h, of ourse, leads to non-exe utability.) Algebrai spe i ation languages
are used for this [3℄. Distributed and parallel omputing problems may require
temporal logi rather than lassi al logi for their spe i ation, and use notations
su h as CSP [6℄, CCS [10℄ or Petri nets.

D. Morris & B. Tamm eds, Pergamon Press, 1991, pp 135-138

37 Appli ation of Logi
Veri ation is done by using an appropriate logi ontaining axioms and inferen erules to dedu e the post- ondition from the pre- ondition [2℄. For ea h onstru t
in the programming language the logi in ludes an inferen e rule whi h de nes
its semanti s. The meaning of the whole onstru t is determined in terms of
the semanti s of its onstituent onstru ts by means of pre- and post onditions
for ea h of the onstru ts involved. Appli ation of these inferen e rules is often
subje t to the satisfa tion of a property, alled a veri ation ondition, whi hrelates some of the pre- and post- onditions.

8 Veri ation Conditions
Program provers are expe ted automati ally to redu e a statement that ertain
ode satis es a given spe i ation to the laim that a parti ular logi al formula
holds. This is done by a veri ation ondition generator and depends on the ode
being annotated suÆ iently with pre- and post- onditions and formulae alled
loop invariants. The inferen e rules for a onstru t do not always enable one todedu e the pre-and post- onditions needed for all the onstituent parts in orderfor the whole onstru t to behave as desired. Those formulae whi h annot bededu ed must be supplied. As noted above, some inferen e rules also involve averi ation ondition that must be satis ed. Combining these yields a logi al
formula upon whi h the orre t fun tioning of the software depends.

9 Theorem Provers
A program prover must now invoke a theorem prover to show that the remaining
logi al formula is always true. Godel showed in the '30s that there is no algorithm that will always establish the validity or otherwise of any formula. Hen ethe theorem prover must either fail o asionally or require human intera tion.
A number of theorem provers are on the market, and they are the entre ofmu h resear h, not just be ause of their appli ation to proving partial orre tness of programs, but also be ause the an be used to dedu e information fromdatabases. Indeed a Prolog system is really just a theorem prover.

10 Termination and Convergen e
The des ription of fun tional spe i ation and veri ation above assumed thatthe ode eventually terminated with some output rather than be oming stu k
in an in nite loop or produ ing an error ondition. Proving the boundedness ofloops involves showing that su essive states at some exit point from the loop
onverge to a state satisfying the exit ondition. When using omplete numbersystems su h as the reals R, this may require appli ation of the usual de nitions
in mathemati al analysis of ontinuity and onvergen e under the appropriate

4

Con ise En y lopedia of Software Engineering

topology. When working with nite sets of the integers, this usually involves awell-ordering of the su essive states, whi h e e tively means asso iating thosestates with a stri tly de reasing sequen e of natural numbers su h a sequen emust be nite. All looping onstru ts have to be he ked, in luding re ursion, andare must be taken to avoid unexpe ted ir uits in linked data stru tures. Careful
programming makes this, and indeed the whole veri ation pro ess, easier.

11 Con urrent Programming
The use of a number of pro essors in distributed or parallel omputing raises
a number of subtle problems to do with onvergen e and termination (see [1℄)whi h do not arise, or are simple, in the sequential ase. Thus, pro esses ompeting for the same resour es ould result in deadlo k through mutual ex lusion,ausing some requested outputs not to be omputed. Liveness is the property
that anything that is supposed to happen eventually does so. This is the proper
generalisation for on urrent pro essing of he king termination in a sequentialsystem. Verifying the liveness of a system is part of applying formal methods.
Not only is the omplete deadlo k of the system to be avoided, but also thelo kout of any individual pro ess.
Another important orre tness property here is that of safety, whi h in thisontext is the generalisation of partial orre tness for a sequential pro ess. Aswell as ea h pro essor performing orre tly with respe t to its fun tional spe i ation there are syn hronisation requirements to satisfy, with onsumers having
to wait for input to be ome available, and onsuming all input in order.

12 Che king Resour es
We have dealt with non-termination above, and now turn to improper termination through the raising of ex eptions. This arises from what may be regarded asrun-time type errors. Typi ally, suÆ ient resour es may not be available. Thus,
the implementations of the reals or integers or the memory may be assumed
in nite for the partial veri ation pro ess des ribed above, whereas in reality
they are not: multipli ation of two over-large numbers gives a result outside theimplemented type Integer. However, if we ensure that the model of omputation
used in the partial veri ation really mat hes in all respe ts the resour es available on the target ma hine, then this kind of type he king is already done aspart of the veri ation pro ess above. In pra ti e, though, it is often useful tota kle these problems separately, espe ially if run-time errors are a eptable.
However, what annot be he ked at that stage are the properties requiredof external obje ts, su h as les to whi h a program may wish a ess. One isthen for ed to verify the whole environment, or be ontent with the possibility ofrun-time errors from this sour e. In parti ular, in this wider ontext, it usually
has to be assumed that the software is ompiled orre tly, and runs on orre t
hardware under a orre t operating system. Clearly, veri ed software an stillD. Morris & B. Tamm eds, Pergamon Press, 1991, pp 135-138

5produ e undesirable output if these assumptions about the orre tness of theenvironment are not met. Indeed, even the veri ation pro ess an be faulty.
It is worth mentioning also that some resour es may vary with time su has hanging diskettes, operating systems, ompilers or even the whole ma hine,
available memory, or power to operate. These an vary over anything from very
short to very long periods, and any veri ation is only valid as long as its presuppositions about those resour es are satis ed.

13 Cost and Limitations
The brief overview of formal methods here shows that some of it requires onsiderable expertise although mu h is straightforward, some an be me hanised but
mu h annot, and it is essentially impossible to guarantee expe ted behaviour
without verifying the omplete system in luding all other software and hardware.
Formal methods are valuable; the more that is he ked the greater on den ethere is in the produ t. However, most systems will be very mu h larger thanan be ompletely veri ed in a reasonable time, and there are so many sour es oferror in veri ation, just as in writing software, that testing will always be partof the validation pro ess. Formal methods provide further tools for in reasing
the reliability of software and hardware, and have the potential for providing
everything that is required, although su h thoroughness is only at great ost.
They an be applied to investigate as many properties as desired, be oming
most ost-e e tive for safety- riti al requirements, for nan ial aspe ts and forheavily used items. Assuming the formal spe i ation is orre t, it is true that
almost without limit, more and more money an be spent to obtain an ever morereliable produ t through formal methods.

14 Related Topi s
There are several losely related items in this volume, most of whi h provide
greater width than has been possible here, des ribing other areas where formality is required to guarantee orre tness against an all-in lusive spe i ation. Inparti ular, the reader is referred to the arti les on
Software Safety and Se urity
Software Spe i ation & Veri ation
Software: The Role of Validation
Spe i ation Languages
System Spe i ation Languages for Hardware Des ription
Translation, Veri ation and Synthesis: A Comparison
Validation and Veri ation of Real Time Software
Of these Software Spe i ation & Veri ation provides greater depth by expanding some of the detail in this arti le. It in ludes examples of formally spe i ed6Con ise En y lopedia of Software Engineering

software using a ouple of spe i ation languages, and the axiomati semanti sof one or two program onstru ts. Hardware des ription languages are usuallysuÆ iently similar to programming languages for mu h of the veri ation pro ess
to be done as for software. If the des ribed hardware is then orre tly translated
automati ally into ir uit diagrams, orre t hardware should result.

Referen es
1. M. Ben-Ari, Prin iples of Con urrent Programming, Prenti e/Hall International,
1982, ISBN 0-13-701078-8.
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. H.Ehrig, B.Mahr, Fundamentals of Algebrai Spe i ation Vols 1,2, SpringerVerlag, 1985, ISBN 3-540-13718-1, and 1990, ISBN 3-540-51799-5.
4. M.J.C. Gordon, The denotational Des ription of Programming Languages,Springer-Verlag, 1979, ISBN 3-540-90433-6.
5. D. Harel, Algorithmi s the Spirit of Computing, Addison-Wesley, 1987, ISBN0-201-19240-3.
6. C. A. R. Hoare, Communi ating Sequential Pro esses, Prenti e/Hall International,
1985, ISBN 0-13-153271-5.
7. 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.
8. C.B. Jones, Systemati Software Development using VDM, (2nd Edition) Prenti e/Hall International, 1990, ISBN 0-13-880733-7.
9. E.G.Manes, M.A.Arbib, Algebrai Approa hes to Program Semanti s, SpringerVerlag, 1986, ISBN 3-540-96324-3.
10. R. Milner, Communi ation and Con urren y, Prenti e/Hall International, 1989,ISBN 0-13-115007-3.
11. M. Spivey, The Z Notation A Referen e Manual, Prenti e Hall, 1989.