Program Transformations And Refinements In HOL
Joakim Wright, Kaisa Sere · 2005
In the refinement calculus, programs are developed in a stepwise fashion by repeated application of transformation rules that preserve total comxtness. We show how such rules can be formalised and proved using the HOL theorem prover. We also show how hierarchies of rules can be built e.g., for parallelising algorithms, and how application of these rules can be automated in HOL. The basis for this work is a formalisation of weakest precondition semantics in higher order logic.