Proving Program Refinements and Transformations

Martin Ward, DPhil Thesis, Oxford University, 1989

[Home] [Publications] [Software] [G.K. Chesterton] [GKC books] [GKC pictures]

Click on each heading to download a gzipped PostScript file with the full text of the chapter.

[Note: the thesis was originally written using a now-obsolete proprietary word processor called Qed. I have converted the files to a crude LaTeX representation of the original using a perl script. These LaTeX files were used to generate the PostScript and PDF files.]

Abstract

In this thesis we develop a theory of program refinement and equivalence which can be used to develop practical tools for program development, analysis and modification. The theory is based on the use of general specifications and an imperative kernel language. We use weakest preconditions, expressed as formulae in infinitary logic to prove refinement and equivalence between programs.

The kernel language is extended by means of ``definitional transformations'' which define new concepts in terms of those already present. The extensions include practical programming constructs, including recursive procedures, local variables, functions and expressions with side-effects. This expands the language into a ``Wide Spectrum Language'' which covers the whole range of operations from general specifications to assignments, jumps and labels. We develop theorems for proving the termination of recursive and iterative programs, transforming specifications into recursive programs and transforming recursive procedures into iterative equivalents. We develop a rigorous framework for reasoning about programs with EXIT statements that terminate nested loops from within; and this forms the basis for many efficiency-improving and restructuring transformations. These are used as a tool for program analysis and to derive algorithms by transforming their specifications. We show that the methods of top-down design and program verification using assertions can be viewed as the application of a small subset of transformations.

Title Page (PDF)

Introduction (PDF)

Chapter 1 (PDF)

Chapter 2 (PDF)

Chapter 3 (PDF)

Chapter 4 (PDF)

Chapter 5 (PDF)

Chapter 6 (PDF)

Chapter 7 (PDF)

Chapter 8 (PDF)

Chapter 9 (PDF)

References (PDF)


[Home] Back to my home page.
Last modified: 18th May 1998
Martin Ward, Software Technology Research Lab, De Montfort University, Leicester.
Email: martin@gkc.org.uk