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 - Feb 1989

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Information Systems
  • Computer Science Applications
  • Computational Theory and Mathematics

Fingerprint Dive into the research topics of 'A language independent proof of the soundness and completeness of generalized Hoare logic'. Together they form a unique fingerprint.

  • Cite this