Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Variables as resource in Hoare Logic

Matthew J. Parkinson, Richard Bornat, and Cristiano Calcagno


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.


Publication typeInproceedings
Published inProceedings of LICS
> Publications > Variables as resource in Hoare Logic