The verification of modules

Grigoris Antoniou

Research output: Contribution to journalArticlepeer-review


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
Issue number2
Publication statusPublished - 1 Mar 1994
Externally publishedYes


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

Cite this