loading...
Variables as Resource in Hoare Logics
Seattle, Washington August 12-August 15
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2006.5221st Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Matthew Parkinson, Middlesex University, UK
Richard Bornat, Middlesex University, UK
Cristiano Calcagno, University of London, UK
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.
Citation:
Matthew Parkinson, Richard Bornat, Cristiano Calcagno, "Variables as Resource in Hoare Logics," lics, pp.137-146, 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.