Refinement concepts formalised in higher order logic
R. J. R. Back, Joakim Wright · Formal Aspects of Computing · 1990
Abstract A theory of commands with weakest precondition semantics is formalised using the HOL proof assistant system. The concept of refinement between commands is formalised, a number of refinement rules are proved and it is shown how the formalisation can be used for proving refinements of actual program texts correct.