Local Reasoning about Data Update

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.