Local Reasoning about Data Update
Venue
Electronic Notes on Theoretical Computer Science, vol. 172, pp. 133–175
Publication Year
2007
Identifiers
Authors
- Cristiano Calcagno
- Philippa Gardner
- Uri Zarfaty
Abstract
We present local Hoare reasoning about data update, using Context Logic for analysing structured data. We apply our reasoning to tree update, heap update which is analogous to local Hoare reasoning using Separation Logic, and term rewriting.