Mechanising Procedures in HOL
Linas Laibinis · 1999
In this paper we present an approach for modelling procedures (as they occur in imperative programs) in a weakest precondition semantics. We show how this approach can be implemented in the mechanisation of the refinement calculus theory in the HOL system. That makes it possible to derive a number of correctness and refinement properties of procedures. Finally, we show how our method for procedure handling can be integrated into a tool for transformational reasoning about programs -- the Refinement Calculator.