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.