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.

In  Proceedings of LICS

Publisher  IEEE

Details