[L2] ================================================ AMAST Links 01 02

                    Interactive Program Derivation
                  Martin Coen - Cambridge University
                          PhD Thesis Abstract
  As programs are increasingly used in safety critical applications,
program correctness is becoming more important; as 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, 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"of's
work in type theory and Manna & 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 denoting
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 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 correctness proofs.
  Thesis now available by anonymous ftp from Cambridge,  at URL: ftp://
ftp.cl.cam.ac.uk/reports/TR272-mc-interactive-program-derivation.dvi.gz