Journal ArticleOPEN ACCESS

Refinement concepts formalised in higher order logic

Formal Aspects of Computing (1990) 2(1) 247-272
DOI: 10.1007/BF01888227
49Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.

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. © 1990 BCS.

Author supplied keywords

Cite

CITATION STYLE

APA

Back, R. J. R., & von Wright, J. (1990). Refinement concepts formalised in higher order logic. Formal Aspects of Computing, 2(1), 247–272. https://doi.org/10.1007/BF01888227

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free