The Transformational Approach to the Development and Verification of Programs in a very High Level Language

Candidate: Deak,Edith Gail


In informal exposition, the correctness of a complex algorithm is often demonstrated by deriving it through successive refinement steps from a high level specification, and supplying proofs of the underlying principles used in the process. However, most existing mechanical program verifiers ignore this standard expository practice, and are generally designed to verify programs written in a low level form. While logically simple algorithms can be handled adequately in this manner, attempting to verify more complex algorithms at a low level requires treatment of implementation details which obscure the main arguments of the verification. This thesis describes a systematic technique for proving algorithms correct using a transformational approach, and presents a detailed transformation/verification scenario of the proof of a variety of complex combinatorial algorithms. The algorithms treated here are considerably more involved than those verified by other methods. The programming language used is a variant of SETL, adapted for program verification, which provides a medium for high level specification. A program P is annotated with logical formulae of set theory, which are called assumptions and assertions. P is said to by partially correct if every computation which satisfies all assumptions also satisfies all assertions. In order to prove the correctness of P, which initially contains only assumptions, we apply proof rules which are used both to transform the program into logical formulae called verification conditions and then to prove these verification conditions. The transformation rules are unique in that they enable the combination of correct program fragments. We are able to reuse general code fragments in a variety of contexts without reproof and to derive several different low level algorithms from a single high level algorithm. The transformations often require proof of enabling conditions. In such cases, when a transformation is performed, the enabling condition is introduced into the program text as an assumption which must be verified in turn using the proof mechanism described above.