HIGHER−LEVEL ALGORITHMIC STRUCTURES IN THE REFINEMENT CALCULUS

Abstract

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.