Context logic and tree update

13 years 5 days ago
Context logic and tree update
Spatial logics have been used to describe properties of treelike structures (Ambient Logic) and in a Hoare style to reason about dynamic updates of heap-like structures (Separation Logic). We integrate this work by analyzing dynamic updates to tree-like structures with pointers (such as XML with identifiers and idrefs). Na?ive adaptations of the Ambient Logic are not expressive enough to capture such local updates. Instead we must explicitly reason about arbitrary tree contexts in order to capture updates throughout the tree. We introduce Context Logic, study its proof theory and models, and show how it generalizes Separation Logic and its general theory BI. We use it to reason locally about a small imperative programming language for updating trees, using a Hoare logic in the style of O'Hearn, Reynolds and Yang, and show that weakest preconditions are derivable. We demonstrate the robustness of our approach by using Context Logic to capture the locality of term rewrite systems. ...
Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where POPL
Authors Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
Comments (0)