Paper: Variables as Resource in Hoare Logics (at LICS 2006)

Authors: Matthew Parkinson Richard Bornat Cristiano Calcagno

Abstract

Hoare logic is bedevilled by complex but coarse side conditions on the use of variables. We define a logic, free of side conditions, which permits more precise statements of a program’s use of variables. We show that it admits translations of proofs in Hoare logic, thereby showing that nothing is lost, and also that it admits proofs of some programs outside the scope of Hoare logic. We include a treatment of reference parameters and global variables in procedure call (though not of parameter aliasing). Our work draws on ideas from separation logic: program variables are treated as resource rather than as logical variables in disguise. For clarity we exclude a treatment of the heap.

BibTeX

  @InProceedings{ParkinsonBornatCalc-VariablesasResource,
    author = 	 {Matthew Parkinson and Richard Bornat and Cristiano Calcagno},
    title = 	 {Variables as Resource in Hoare Logics},
    booktitle =  {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)},
    year =	 {2006},
    month =	 {August}, 
    pages =      {137--146},
    location =   {Seattle, Washington, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }