Formal Aspects of Computing · 1990 · 61 citations · 6 references
HumanitiesComputer ScienceFormal MethodsLogicSemanticsCompositional SemanticsFormal SemanticsMathematical LogicModel TheoryPredicate LogicRefinement CalculusHigher-order LogicHigher-order Logic ReasoningModel RefinementRefinementRefinement Checking
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.
6
A calculus of refinements for program derivations
R. J. R. Back · Acta Informatica · 1988 · 247 citations