From: Todd D Millstein (todd@cs.washington.edu)
Date: Mon Dec 02 2002 - 09:52:10 PST
Bob Harper mentioned to me this work that John Reynolds has done recently
on "separation logic," a logic for reasoning about shared mutable data
structures (and the heap in general). I recently got time to take a look
and found it quite nice, so I thought I'd share it with you.
The paper I read was presented at LICS this year and is at
ftp://ftp.cs.cmu.edu/user/jcr/seplogic.ps.gz
Before you hit delete, though, this is the most readable LICS paper I've
ever seen! It's easy to get the main idea of what's going on (even if the
details are not understood on the first pass).
The basic idea is that reasoning about mutation just in plain first-order
logic is tedious, cumbersome, and global (see below). So what they do is
add some new primitive propositions and connectives to the logic, that
explicitly talk about the heap. In particular, the notion of two portions
of the heap being disjoint (i.e. separated) is a first-class citizen in
the logic. He shows how to use these new entities to talk very succinctly
about sharing properties of data structures, etc.
One nice thing about these new connectives is that they satisfy all kinds
of algebraic properties (e.g. distributivity), making them easy to
manipulate to prove things. And he shows how to extend a Hoare-style
weakest precondition semantics to this kind of logic, to reason about
programs that manipulate the heap.
You might think the new primitives don't buy you anything, because they
can just be desugared into regular first-order formulas, but it turns out
that that's not exactly the case (although I don't understand the
details). One really nice advantage of the new logic is that there's an
implicit frame axiom whereby heap locations that are not mentioned are
implicitly unchanged. This is not given for free in traditional
first-order logic, where you instead have to explicitly state (and reason
about) these kinds of things. So in some sense the new logic allows
formulas to be more local.
Todd
_______________________________________________
Cecil mailing list
Cecil@cs.washington.edu
http://mailman.cs.washington.edu/mailman/listinfo/cecil
This archive was generated by hypermail 2.1.5 : Mon Dec 02 2002 - 09:52:14 PST