A language independent proof of the soundness and completeness of generalized Hoare logic

Patrick Cousot, Radhia Cousot

Research output: Contribution to journalArticle

Abstract

Generalized Hoare logic (GHL) is a formal logical system for proving invariance properties of programs. It was first introduced by Lamport to reason about simple concurrent programs with shared variables. It was generalized by Lamport and Schneider who noticed that the inference rules for each language construct (enabling invariance properties of statements to be derived from invariance properties of their components) can be viewed as special cases of simple logical meta-rules. We give a rigorous definition of GHL, based upon an abstract formal-ization of the syntax and semantics of programs so as to provide an interpretation for formulas of GHL which is independent of the specific instructions of the programming language used. We prove that the proof system of GHL is sound and relatively complete under hypotheses, which we formulate independently of any programming language; these are simple conditions which relate the axiom schemata for atomic actions and the axiom schemata, which define the control flow semantics, to the semantics of programs.

Original languageEnglish (US)
Pages (from-to)165-191
Number of pages27
JournalInformation and Computation
Volume80
Issue number2
DOIs
StatePublished - 1989

Fingerprint

Soundness
Invariance
Completeness
Semantics
Logic
Computer programming languages
Axiom
Schema
Programming Languages
Flow control
Inference Rules
Proof System
Flow Control
Acoustic waves
Concurrent
Language

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

A language independent proof of the soundness and completeness of generalized Hoare logic. / Cousot, Patrick; Cousot, Radhia.

In: Information and Computation, Vol. 80, No. 2, 1989, p. 165-191.

Research output: Contribution to journalArticle

@article{71538e4af6ca497ea06d1d78b137f7d5,
title = "A language independent proof of the soundness and completeness of generalized Hoare logic",
abstract = "Generalized Hoare logic (GHL) is a formal logical system for proving invariance properties of programs. It was first introduced by Lamport to reason about simple concurrent programs with shared variables. It was generalized by Lamport and Schneider who noticed that the inference rules for each language construct (enabling invariance properties of statements to be derived from invariance properties of their components) can be viewed as special cases of simple logical meta-rules. We give a rigorous definition of GHL, based upon an abstract formal-ization of the syntax and semantics of programs so as to provide an interpretation for formulas of GHL which is independent of the specific instructions of the programming language used. We prove that the proof system of GHL is sound and relatively complete under hypotheses, which we formulate independently of any programming language; these are simple conditions which relate the axiom schemata for atomic actions and the axiom schemata, which define the control flow semantics, to the semantics of programs.",
author = "Patrick Cousot and Radhia Cousot",
year = "1989",
doi = "10.1016/0890-5401(89)90018-7",
language = "English (US)",
volume = "80",
pages = "165--191",
journal = "Information and Computation",
issn = "0890-5401",
publisher = "Elsevier Inc.",
number = "2",

}

TY - JOUR

T1 - A language independent proof of the soundness and completeness of generalized Hoare logic

AU - Cousot, Patrick

AU - Cousot, Radhia

PY - 1989

Y1 - 1989

N2 - Generalized Hoare logic (GHL) is a formal logical system for proving invariance properties of programs. It was first introduced by Lamport to reason about simple concurrent programs with shared variables. It was generalized by Lamport and Schneider who noticed that the inference rules for each language construct (enabling invariance properties of statements to be derived from invariance properties of their components) can be viewed as special cases of simple logical meta-rules. We give a rigorous definition of GHL, based upon an abstract formal-ization of the syntax and semantics of programs so as to provide an interpretation for formulas of GHL which is independent of the specific instructions of the programming language used. We prove that the proof system of GHL is sound and relatively complete under hypotheses, which we formulate independently of any programming language; these are simple conditions which relate the axiom schemata for atomic actions and the axiom schemata, which define the control flow semantics, to the semantics of programs.

AB - Generalized Hoare logic (GHL) is a formal logical system for proving invariance properties of programs. It was first introduced by Lamport to reason about simple concurrent programs with shared variables. It was generalized by Lamport and Schneider who noticed that the inference rules for each language construct (enabling invariance properties of statements to be derived from invariance properties of their components) can be viewed as special cases of simple logical meta-rules. We give a rigorous definition of GHL, based upon an abstract formal-ization of the syntax and semantics of programs so as to provide an interpretation for formulas of GHL which is independent of the specific instructions of the programming language used. We prove that the proof system of GHL is sound and relatively complete under hypotheses, which we formulate independently of any programming language; these are simple conditions which relate the axiom schemata for atomic actions and the axiom schemata, which define the control flow semantics, to the semantics of programs.

UR - http://www.scopus.com/inward/record.url?scp=0024611995&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0024611995&partnerID=8YFLogxK

U2 - 10.1016/0890-5401(89)90018-7

DO - 10.1016/0890-5401(89)90018-7

M3 - Article

AN - SCOPUS:0024611995

VL - 80

SP - 165

EP - 191

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 2

ER -