Logic in Computer Science (LICS 1988)

Paper: On the existence of effective Hoare logics (at LICS 1988)

Authors: Michal Grabowski Hardi Hungar

Abstract

Every proof system for (partial) correctness yields an enumeration procedure for correctness assertions. Other researchers have proved results on the existence of (sound and complete) enumeration procedures for assertions about programs from an acceptable programming language where the assertion language is first-order logic. It is shown that some of the assumptions are stronger than necessary, whereas others must not be weakened. Two novel procedures are given that work for more interpretations with a smaller oracle than those known up to now

BibTeX

  @InProceedings{GrabowskiHungar-Ontheexistenceofeff,
    author = 	 {Michal Grabowski and Hardi Hungar},
    title = 	 {On the existence of effective Hoare logics},
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {428--435},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }