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.

LanguageEnglish
Pages223-244
Number of pages22
JournalFormal Aspects of Computing
Volume6
Issue number2
DOIs
Publication statusPublished - 1 Mar 1994
Externally publishedYes

Fingerprint

Module
Correctness
Assertion
Calculus
Logic
Partial
Concepts

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 = "3",
day = "1",
doi = "10.1007/BF01221100",
language = "English",
volume = "6",
pages = "223--244",
journal = "Formal Aspects of Computing",
issn = "0934-5043",
publisher = "Springer London",
number = "2",

}

The verification of modules. / Antoniou, Grigoris.

In: Formal Aspects of Computing, Vol. 6, No. 2, 01.03.1994, p. 223-244.

Research output: Contribution to journalArticle

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 - http://www.scopus.com/inward/record.url?scp=34249766306&partnerID=8YFLogxK

U2 - 10.1007/BF01221100

DO - 10.1007/BF01221100

M3 - Article

VL - 6

SP - 223

EP - 244

JO - Formal Aspects of Computing

T2 - Formal Aspects of Computing

JF - Formal Aspects of Computing

SN - 0934-5043

IS - 2

ER -