The verification of modules

Grigoris Antoniou

doi:10.1007/BF01221100

The verification of modules

Grigoris Antoniou

Research output: Contribution to journal › Article › peer-review

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 language	English
Pages (from-to)	223-244
Number of pages	22
Journal	Formal Aspects of Computing
Volume	6
Issue number	2
DOIs	https://doi.org/10.1007/BF01221100
Publication status	Published - 1 Mar 1994
Externally published	Yes

Access to Document

10.1007/BF01221100Licence: Unspecified

Cite this

@article{99b8521e1e204e19848a16906d0c823c,

title = "The verification of modules",

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.",

keywords = "Algebraic interfaces, D.2 [Software Engineering]: D2.2 Tools and Techniques, D2.4 Program Verification, F.3 [Logics and Meanings of Programs]: F3.1 Specifying and Verifying and Reasoning about Programs, Hoare logic, Modules, Verification",

author = "Grigoris Antoniou",

year = "1994",

month = mar,

day = "1",

doi = "10.1007/BF01221100",

language = "English",

volume = "6",

pages = "223--244",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Association for Computing Machinery (ACM)",

number = "2",

}

TY - JOUR

T1 - The verification of modules

AU - Antoniou, Grigoris

PY - 1994/3/1

Y1 - 1994/3/1

N2 - 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.

AB - 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.

KW - Algebraic interfaces

KW - D.2 [Software Engineering]: D2.2 Tools and Techniques

KW - D2.4 Program Verification

KW - F.3 [Logics and Meanings of Programs]: F3.1 Specifying and Verifying and Reasoning about Programs

KW - Hoare logic

KW - Modules

KW - Verification

UR - https://www.scopus.com/pages/publications/34249766306

U2 - 10.1007/BF01221100

DO - 10.1007/BF01221100

M3 - Article

AN - SCOPUS:34249766306

SN - 0934-5043

VL - 6

SP - 223

EP - 244

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 2

ER -

The verification of modules

Abstract

Access to Document

Other files and links

Fingerprint

Cite this