Paper: Floyd-Hoare Logic Defines Semantics: Preliminary Version (at LICS 1986)

Authors: Albert R. Meyer

Abstract

The first-order partial correctness assertions provable in Floyd-Hoare logic about an uninterpreted while-program scheme determine the scheme up to equivalence. This settles an open problem of Meyer and Halpern. The simple proof of this fact carries over to other partial correctness axiomatizations given in the literature for wider classes of Algol-like program schemes.

BibTeX

  @InProceedings{Meyer-FloydHoareLogicDefi,
    author = 	 {Albert R. Meyer},
    title = 	 {Floyd-Hoare Logic Defines Semantics: Preliminary Version},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {44--48 },
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }