Frames, Footprints,

Local Action, etc

 

The frame problem in AI is that, when specifying what changes, an inordinate amount of effort usually needs to be spent saying what doesn't change. These frame axioms (what doesn't change) distract from the real concern: what changes. For example, when say you increment location 10's contents, you intend that no other locations are altered, but it is a pain to say so explicitly. There are many, many papers on the frame problem in the AI literature. You can find them on search engines. Papers of Reiter are particularly recommended, for their simplicity and clarity.

A POPL'01 paper and a CSL'01 paper described an approach to the frame problem for programs based on a connection between frame axioms and the notion of footprint : the cells a program accesses. We know that any cell outside the footprint will not change, so frame axioms describing this absence of change can be obtained for free, without explicitly stating them beforehand. A FOSSACS'02 paper went on to explain that, while separation logic gives a convenient way to exploit this fact, using the frame rule,



it is in no way necessary: the frame axioms (invariants for cells outside the footprint) are just true, whether or not you employ separation logic to express them. Indeed, approaches to footprints/frames that do not use separation logic - but that rely on something close to these semantic underpinnings - have been described by Kassios, Smans, Banerjee, Naumann and others; you can find them on the web. 

The frame rule is the key to modular reasoning about programs in separation logic, and its automation is the workhorse of program analysis tools such as Smallfoot, Space Invader and Abductor.

Finally, several papers have taken these ideas further, and probed more deeply.

  1. Local Action and Abstract Separation Logic.. C Calcagno, PW O'Hearn and H Yang. In LICS'07.

  2. Local Reasoning about Data Update P Gardner, C Calcagno and U Zarfaty. Gordon Plotkin's festschrift, ENTCS 2007.

  3. Footprints in Local Reasoning. M Raza and P Gardner. In LMCS (FOSSACS 2008 Special Issue).