Can we ever be sure that our computer programs will work reliably? One approach to this problem is to attempt a mathematical proof of reliability, and this has led to the idea of Formal Methods: if you have a formal, logical specification of the properties meant by 'working reliably', then perhaps you can give a formal mathematical proof that the program (presented as a formal text) satisfies them.
Of course, this is by no means trivial. Before we can even get started on a formal proof we must turn the informal ideas intended by 'working reliably' into a formal specification, and we also need a formal account of what it means to say that a program satisfies a specification (this amounts to a semantics of the programming language, an account of the meaning of programs). None the less, Formal Methods are now routinely practised by a number of software producers.
The aim of this book is to present informal formal methods, showing the benefits of the approach even without strict formality although we use logic as a notation for the specifications, we rely on informal semantics – a programmer's ordinary intuitions about what small, linear stretches of code actually do – and we use proofs to the level of rigour of ordinary mathematics.
This can, of course, serve as a first introduction to strict Formal Methods, but it should really be seen much more broadly. The benefits of Formal Methods do not accrue just from the formality. The very effort of writing a specification prior to the coding focuses attention on what the user wants to get out of the program, as opposed to what the computer has to do, and the satisfaction proof, even if informal, expresses our idea of how the algorithm works. This does not require support tools, and the method – which amounts really to methodical commenting – is practicable in all programming tasks.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.