Programming Research Group Technical Monograph PRG-124

Steve King

January 1999, 165 pages

This thesis extends the refinement calculus into two new areas: exceptions and iterators. By extending the calculus in this way, it is shown that we can carry out the formal development of programs which exploit the exception-handling and iterator mechanisms of programming languages. For both areas of expansion, the same strategy is used: relatively simple extensions to the language are first proposed, together with the semantic machinery to prove the correctness of new laws. Then these simple extensions are combined into complex mechanisms which mimic more closely the language facilities found in programming languages, which are necessary for programs of realistic size.

For exceptions, the major idea is to distinguish between normal and exceptional termination of program constructs. Dijkstra's weakest precondition semantics are extended to give meaning to this by considering predicate transformers which take as arguments more than one postcondition. The notation is extended to deal with multiple exceptions, and appropriate actions for them, by use of procedures.

The technical background for the iterator construct proposed comes from the functional programming community: homomorphisms from initial data types. Again, it is shown how this can be related to iterators in programming languages. This involves giving weakest precondition semantics for procedure as parameters.

Both extensions to the refinement calculus are used to give formal developments of programs which use a pre-existing library of abstract data types. A specification is given for a typical library component, and several sample programs are developed.