Procedures and recursion in the refinement calculus

Abstract

This thesis looks at ways to deal with procedures and recursion in the refinement calculus. It considers approaches from Back and Morgan, which differ primarily in what they allow to be parametrised. Cavalcanti, Sampaio and Woodcock (CSW) claim to have identified a problem with Morgan's treatment of procedures and parameters, and the thesis spends some time responding to this argument. The thesis then looks at recursion, considering not only the theory of handling recursive procedures, but also the practicalities of dealing with them. We look at the different approaches used by Back and Morgan, and then consider some refinement laws CSW have provided for working with recursive procedures. Finally, the thesis considers how to work with mutual recursion. Hesselink gives a theorem which can be used to prove total correctness of programs containing mutual recursion, unlike many who write about recursion. We consider how to modify this theorem to work within the approach to procedures that we have settled on. This results in two modifications of his theorem, and a refinement law, along with examples demonstrating their use.