Local Reasoning about Data Update
Cristiano Calcagno, Philippa Anne Gardner, Uri Zarfaty · Electronic Notes in Theoretical Computer Science · 2007
We present local Hoare reasoning about data update, introducing Context Logic for analysing structured data. We apply our reasoning to tree update, heap update, and term rewriting. Our reasoning about heap update is exactly analogous to the local Hoare reasoning of Separation Logic. Our reasoning about tree update and term rewriting can only be done with Context Logic.