Mechanising some Advanced Refinement Concepts

We describe how proof rules for three advanced refinement features are mechanically verified using the HOL theorem prover. These features are data refinement, backwards data refinement and superposition refinement of initialised loops. We also show how applications of these proof rules to actual program refinement can be checked using the HOL system, with the HOL system generating the verification conditions. 1 Introduction Stepwise refinement is a methodology for developing programs from high-level program specifications into efficent implementations. The refinement calculus of Back [1, 2] is a formalisation of this approach, based on the weakest precondition calculus of Dijkstra [9]. Practical program derivation within the refinement calculus [5] has shown that refinement steps often tend to be very similar to each other. Rather than always inventing a refining statement and proving the correctness of the refinement, it is convenient to have access to a collection of program transfo..