## Peter O'Hearn

### BI as an Assertion Language for Mutable Data Structures

Reynolds has recently developed a logic for reasoning about mutable
data structures, where pre- and post-conditions are written in an
intuitionistic logic enriched with a spatial form of conjunction. We
investigate the approach from the point of view of the logic BI of
O'Hearn and Pym. We begin by giving a model in which the law of the
excluded middle holds, thus showing that the approach is compatible
with classical logic. The relationship between the intuitionistic
and classical versions of the system is established by a
translation, analogous to a translation of intuitionistic
logic into the modal logic S4. We also consider the question of
completeness of the axioms. BI's spatial implication is used to
formulate an axiom expressing the weakest pre-condition for
object-component assignments, and an axiom for allocating a cons cell is
shown to be complete only under an interpretation of triples that
allows a command to be applied to states with dangling pointers. We
make this latter a feature, by incorporating an operation, and axiom, for
disposing of memory. Finally, we describe a local character enjoyed
by specifications in the logic, and show how this enables a class of
frame axioms, which say what parts of the heap don't change, to be
inferred automatically.

This is joint work with Samin Ishtiaq.

May 3, 2000

3:30pm

Wean 8220