Refinement Concepts Formalized in Higher Order Logic.
Ralph‐Johan Back · 1990
A theory of commands with weakest precondition semantics is formalized using the HOL proof assistant system. The concept of refinement between commands is formalized, a number of refinement rules are proved and it is shown how the formalization can be used for proving refinements of actual program texts correct. 1 Introduction The refinement calculus is a theory of program transformations that preserve the total correctness of programs. It was first described in [Ba78, Ba80] and has been further elaborated in [Ba88a, Ba88b, MoRoGa88, Morr87]. It is based on the weakest precondition technique of [Di76]. The refinement calculus has been used as a tool for stepwise refinement of sequential algorithms, and recently also for the derivation of parallel algorithms from sequential algorithms [BaSe89, Wr89]. The HOL system (Higher Order Logic) is a theorem proving assistant, which can be used to formalize theories and verify proofs of theorems within these theories. It is based on the LCF syst...