Introduction

Formal methods of software verification, which involve mathematical reasoning about the properties of software, have the potential to greatly increase the quality of systems involved in high-risk areas (in terms of both cost and safety). Huth and Ryan [25] suggest that formal methods may encourage better documentation and reduce time and money spent on software maintenance, and that software developed or verified formally may be more easily reusable, and rigorous guarantees of critical performance can be proven. Examples of the failure of software which have impacted human safety include Leveson's documentation of the Therac-25 medical device [31], a radiation therapy machine which dangerously overdosed six people in the 1980's. See also [40].

The traditional method of formal software verification starts with an existing program, and an attempt to prove that the program meets this specification is made. This involves the verifier (usually human) finding proof structures (for example induction) that match the structure of the program. This becomes increasingly complex as the size of the program increases, and has not been embraced rapidly by industry [24,28], and is most commonly abandoned in favour of informal software testing (a search for cases where the program does not meet its specification). Common methods used include static checking for forms of code that commonly result in deviations from intended behaviour [30,20], and iterative development with regression testing (see page 504 in [51]).

An alternative method is suggested by Martin-Löf [35], who describes the connection between constructive mathematics and programming. More concrete instances of this are mentioned by Hoare [53]. This leads to an interesting new programming paradigm:

1. Construct a formal logic
2. Write a formal specification of the program
   (a logical statement to be proven)
3. Build a formal proof of the specification in that logic
4. Process this proof into an executable program

Assuming that the logic is consistent, then step 3 can be mechanically verified (or built in such a way that verification is implicit). This requires that the proof be sufficiently ``formal''- each proof step is an application of an axiom or a previously proven theorem. Then if the translation in step 4 is correct, the output program must be ``correct'' (i.e. it meets the formal specification). The formalism of the proof also helps to remove any ambiguity that may confuse this final step.

This has been investigated by many, including Bates and Constable [11]. Albrecht and Crossley [3], and Crossley and Poernomo [18] have been exploring the idea of extracting programs from semi-formal proofs which are similar to the proofs written by humans in mathematics books.

A major problem with this method of constructing programs from proofs is the difficulty with which people have writing formal proofs in step 3, having been taught to omit the statement of routine logical steps and rely on the intuition of the reader to infer these.

We begin by giving a brief background of formal theorem-proving with the aid of computer software in the following chapter. In chapter three we define the goals this project sets out to achieve. Next an account of the structure and operation of the product of the project, the Igloo theorem proving interface, is given. Then we compare a proof in Igloo to a human-written proof before concluding the discussion of the project, and suggesting directions for further work.