|
Published Articles >> Table of Contents >> Abstract
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)
pp. 137-146
Variables as Resource in Hoare Logics
Matthew Parkinson, Middlesex University, UK
Richard Bornat, Middlesex University, UK
Cristiano Calcagno, University of London, UK
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2006.52
Send link to a friend
| 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.
|
 Additional Information
|
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
|
|
