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

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.