Home

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!)

By neelk at 2007-02-02 22:41 | Semantics | other blogs | 8231 reads

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?

By Dave Herman at Sat, 2007-02-03 00:02 | login or register to post comments

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.

By neelk at Sat, 2007-02-03 17:41 | login or register to post comments

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.

By Ehud Lamm at Sat, 2007-02-03 19:03 | login or register to post comments

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.

By Paul Snively at Sun, 2007-02-04 05:34 | login or register to post comments

Trouble with the link?

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

By Hank Thediek at Sat, 2007-02-03 00:18 | login or register to post comments