### 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 language | English (US) |
---|---|

Pages (from-to) | 165-191 |

Number of pages | 27 |

Journal | Information and Computation |

Volume | 80 |

Issue number | 2 |

DOIs | |

State | Published - 1989 |

### Fingerprint

### ASJC Scopus subject areas

- Computational Theory and Mathematics

### Cite this

*Information and Computation*,

*80*(2), 165-191. https://doi.org/10.1016/0890-5401(89)90018-7

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

Research output: Contribution to journal › Article

*Information and Computation*, vol. 80, no. 2, pp. 165-191. https://doi.org/10.1016/0890-5401(89)90018-7

}

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 -