The verification of modules

Research output: Contribution to journalArticle

Abstract

We present a module concept with algebraic interfaces and imperative implementation. It is shown that under some natural conditions, module correctness may be expressed in Hoare logic as a partial correctness assertion. Also, we discuss questions of practical verification of modules using Hoare's calculus.

Original languageEnglish
Pages (from-to)223-244
Number of pages22
JournalFormal Aspects of Computing
Volume6
Issue number2
DOIs
Publication statusPublished - 1 Mar 1994
Externally publishedYes

Fingerprint Dive into the research topics of 'The verification of modules'. Together they form a unique fingerprint.

  • Cite this