Local Reasoning about Data Update

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.

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
• Keywords: Context Logic, ENTCS 2007, Local Hoare Reasoning, Update