P. Cousot and R. Cousot, A language independent proof of the soundness and completeness of generalized Hoare logic

Patrick Cousot and Radhia Cousot.
A language independent proof of the soundness and completeness of generalized Hoare logic.
In Information and computation 80 (2):165—191 (1989).
© 1989 Elsevier Science B.V. All rights reserved.
PDF (1297 Kb)
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.

Bibliography:

@article{CousotCousot89-IC,
   author =  {Cousot, P{.} and Cousot, R{.}},
   title =   {A language independent proof of the soundness 
              and completeness of generalized {H}oare logic},
   journal = {Information and Computation},
   volume =  80,
   number =  2,
   pages =   {165--191},
   month =   feb,
   year =    1989,
}

\bibitem{CousotCousot89-IC}
P{.} Cousot and R{.} Cousot.
\newblock A language independent proof of the soundness 
          and completeness of generalized {H}oare logic.
\newblock {\em Information and Computation}, 80(2):165--191, 1989.

copyright notice
Last modified: Monday, 04-Jan-2010 13:11:07 CET