On 11/3/10 11:15 PM, Ben Karel wrote: > Separation logic I don't know much about, but my impression is that it > optimizes for mathematical tractability over human comprehensibility.
Separation logic is pretty straightforward IMO. The idea is that you have some language of predicates over heaps (e.g., this heap is well-formed, this heap has such and such shape,...) and then separation logic gives you tools for manipulating those predicates (which are considered essentially as atomic formulae wrt the separation logic). In particular you get the connective _*_. What it means is that if P*Q is true of some heap H, then H can be partitioned into two heaps H' and H'' such that P is true of H' and Q is true of H''. The other main connective is a form of implication _-*_ where P-*Q is true of H provided that if you give me a chunk of heap where P is true, H', then Q will be true of the combined H and H' heap (though P need not be true of the composite). These are often used together in the idiom P * (Q -* R) which captures the idea that if we can change P into Q (for some sub-heap) then R will be the case (for the whole). While _-*_ can be a bit odd to comprehend, the _*(_-*_) idiom is the most common use of it, and the idiom is quite easy to internalize. That's basically all there is to it. The tricky part is figuring out what language of predicates you're interested in, and how to make sure your deductions in separation logic track the computation of your programs. One option for the latter is to use Hoare Type Theory, which is far from trivial. -- Live well, ~wren _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
