Paper: True Relative Completeness of an Axiom System for the Language L4 (Abridged) (at LICS 1986)

Authors: Steven M. German Edmund M. Clarke Joseph Y. Halpern

Abstract

A completeness proof for a logic of programs often involves analysis and techniques that give insight into the semantics of the language, and so are of independent interest. In a previous paper, we introduced an axiom system for partialcorrectness assertions in an Agol-like language with procedures passed as parameters, but with no global variables. Sound and relatively complete axiom systems for languages with these features had been sought by a number of researchers, but previous to [GCH83], all of the published solutions had been unsatisfactory in various technical ways. We discuss a proof that the axiom system is sound and relatively complete in the sense of Cook. Because previous relative completeness proofs for languages with procedures as parameters have been extremely complicated, it is noteworthy that we are now able to present a proof in a somewhat simpler form. Details of the proof are of interest, because we introduce techniques for dealing with the semantics of Agol-like languages that are useful beyond the immediate problem of the language L4. We also prove a new incompleteness result that applies to our logic and to similar Hoare logics.

BibTeX

  @InProceedings{GermanClarkeHalpern-TrueRelativeComplet,
    author = 	 {Steven M. German and Edmund M. Clarke and Joseph Y. Halpern},
    title = 	 {True Relative Completeness of an Axiom System for the Language L4 (Abridged)},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {11--25},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }