Joint work with Cristiano Calcagno and Uri Zarfaty.

Structured data update is pervasive in computer systems: examples include heap update on local machines, information storage on hard discs, the update of distributed XML databases, and general term rewriting systems. Programs for manipulating such dynamically-changing data are notoriously difficult to write correctly. Hoare Logics provide a standard technique for reasoning about such update. Hoare reasoning has been widely studied for heap update, from the original work of Hoare based on first-order logic to the recent work of O'Hearn, Reynolds and Yang with their emphasis on local reasoning using Separation Logic. Hoare reasoning has hardly been explored for other data structures.

We have recently shown that the techniques for reasoning locally about heap update can be adapted to reason locally about tree update (XML update). Surprisingly, the Ambient Logic for reasoning locally about trees is not expressive enough to capture such update reasoning. Instead, we had to fundamentally change the way we reason about structured data, by developing Context Logic for analysing both data and contexts. Local data update typically identifies the portion of data to be replaced, removes it, and inserts the new data in the same palce. This place of insertion -- or context -- is essential for reasoning about update. Given the conceptual nature of our context reasoning, Context Logic will apply to a wide range of structured data.

In this talk, I will introduce Context Logic, illustrating how it generalises Separation Logic and its general theory Bunched Logic. I will show how to use Context Logic as a basis for local Hoare reasoning about:

• a simple imperative programming language for updating trees (XML);
• heap update where our reasoning is exactly analogous to the reasoning using Separation logic; and
• term rewriting systems which escaped reasoning using Separation Logic.

A striking point is that our Hoare reasoning is similar in all these examples, which suggests that it should be possible to develop a unified theory of update using Context Logic.