Separation Logic: A Logic for Shared Mutable Data Structures

Separation Logic: A Logic for Shared Mutable Data Structure, John C. Reynolds. LICS 2002

In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure.

The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a "separating conjunction" that asserts that its subformulas hold for disjoint parts of the heap, and a closely related "separating implication". Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing.

I think this paper has been mentioned several times in discussion on LtU, but never gotten an article of its own. It's a really elegant piece of work that addresses the biggest weakness of Hoare logic: that you cannot do local, modular correctness proofs of programs that use aliasable state.

(I should say my own research is on using separation logic in languages like ML or Haskell, so I am a partisan!)

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I'll bite

Why Haskell? For enriching the rather inexpressive monadic sub-language?

A monad lets you nicely

A monad lets you nicely isolate your imperative code and put it in its own little box, but you still need to reason about your monadic code, and so you still need the ability to reason about mutation and aliasing and so on.

you still need to reason

you still need to reason about your monadic code

This is an important point that people often downplay when discussing functional programming.

Tie-In

I think this point dovetails neatly with Mark Miller's comment about lightweight static capabilities. The point is that you can use Coq or whatever to prove properties about what might be a very small module, but that module participates in the type system in such a way that the invariants proven about it are guaranteed to be maintained by the abstraction boundary. This seems like a key point to me as well.

Trouble with the link?

Trouble with the link? Gives me an error.
Edit: Oh, it's an ftp site.