J.S. Fitzgerald
P.A. Lindsay
R. Moore
University of Newcastle upon Tyne. 1992
This paper concerns the construction of formal proofs of conjectures arising in model-oriented specification. It is argued that the process of constructing a formal proof, whether by hand or with help of a mechanical prover, benefits both from a careful consideration of a rigorous form of the proof prior to formalization and from the availability of a library of useful, formally-proved results. These points are illustrated on a simple VDM specification. It is first shown how informal argument or an attempt at the rigorous proof of a satisfiability obligation can lead to the discovery of errors in the original specification. A complete rigorous proof of the satisfiability obligation for the corrected specification is then given. The task of making this proof fully formal is then considered, and insight gained by this process is applied to simplifying the rigorous proof so that it can make use of existing results from a library of already-proven theorems. Although the work described here has been carried out using the Vienna Development Method's specification language and logic, the points made are by no means specific to that formalism.