Refinement concepts formalised in higher order logic
- 1 March 1990
- journal article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 2 (1), 247-272
- https://doi.org/10.1007/bf01888227
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.This publication has 14 references indexed in Scilit:
- Refinement calculus, part I: Sequential nondeterministic programsLecture Notes in Computer Science, 1990
- Mechanizing Programming Logics in Higher Order LogicPublished by Springer Nature ,1989
- A lattice-theoretical basis for a specification languageLecture Notes in Computer Science, 1989
- Stepwise refinement of action systemsLecture Notes in Computer Science, 1989
- A calculus of refinements for program derivationsActa Informatica, 1988
- A theoretical basis for stepwise refinement and the programming calculusScience of Computer Programming, 1987
- Soundness of Hoare's logic: an automated proof using LCFACM Transactions on Programming Languages and Systems, 1987
- A simple fixpoint argument without the restriction to continuityActa Informatica, 1986
- On the semantics of fair parallelismPublished by Springer Nature ,1980
- A lattice-theoretical fixpoint theorem and its applicationsPacific Journal of Mathematics, 1955