Semantic Analysis of Pointer Aliasing, Allocation and Disposal in Hoare Logic
Cristiano Calcagno, Samin Ishtiaq and Peter W. O'Hearn
To appear at the 2nd International Conference on Principles and Practice of
Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000
Bornat has recently described an approach to reasoning about
pointers, building on work of Morris.
Here we describe a semantics that validates the approach, and
use it to help devise axioms for operations that allocate and
dispose of memory.