Computer Laboratory

Technical reports

Interactive program derivation

Martin David Coen

November 1992, 100 pages

This technical report is based on a dissertation submitted March 1992 by the author for the degree of Doctor of Philosophy to the University of Cambridge, St John’s College.

Abstract

As computer programs are increasingly used in safety critical applications, program correctness is becoming more important; as the size and complexity of programs increases, the traditional approach of testing is becoming inadequate. Proving the correctness of programs written in imperative languages is awkward; functional programming languages, however, offer more hope. Their logical structure is cleaner, and it is practical to reason about terminating functional programs in an internal logic.

This dissertation describes the development of a logical theory called TPT for reasoning about the correctness of terminating functional programs, its implementation using the theorem prover Isabelle, and its use in proving formal correctness. The theory draws both from Martin-Löf’s work in type theory and Manna and Waldinger’s work in program synthesis. It is based on classical first-order logic, and it contains terms that represent classes of behaviourally equivalent programs, types that denote sets of terminating programs and well-founded orderings. Well-founded induction is used to reason about general recursion in a natural way and to separate conditions for termination from those for correctness.

The theory is implemented using the generic theorem prover Isabelle, which allows correctness proofs to be checked by machine and partially automated using tactics. In particular, tactics for type checking use the structure of programs to direct proofs. Type checking allows both the verification and derivation of programs, reducing specifications of correctness to sets of correctness conditions. These conditions can be proved in typed first-order logic, using well-known techniques of reasoning by induction and rewriting, and then lifted up to TPT. Examples of program termination are asserted and proved, using simple types. Behavioural specifications are expressed using dependent types, and the correctness of programs asserted and then proved. As a non-trivial example, a unification algorithm is specified and proved correct by machine.

The work in this dissertation clearly shows how a classical theory can be used to reason about program correctness, how general recursion can be reasoned about, and how programs can direct proofs of correctness.

Full text

PDF (0.6 MB)
DVI (0.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-272,
  author =	 {Coen, Martin David},
  title = 	 {{Interactive program derivation}},
  year = 	 1992,
  month = 	 nov,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-272.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-272}
}