Home

Expressing Heap-shape Contracts in Linear Logic

Expressing Heap-shape Contracts in Linear Logic, Frances Perry, Limin Jia, David Walker.

Contracts (dynamically checked programmer assertions) are a widely accepted mechanism for specifying, checking and documenting properties of software components. Most, if not all, contract systems expect programmers to use the native programming language to express their program invariants. While this is most effective for many simple invariants, expressing properties of data structures and aliasing patterns can be extremely complicated. If written in the native language in an unstructured way, such contracts are bound to be unclear and ineffective as documentation.

In this paper, we show how to use linear logic as a language of contracts for an imperative programming language. The high-level nature of our linear logical contracts makes specifying memory shape and aliasing properties of complex recursive data structures easy. Moreover, since we give our logic a clear, compositional semantics, the contracts serve as effective, executable documentation for programmer expectations. In order to evaluate the truth of our linear logical contracts at run time, we use a modifed version of LolliMon, a linear logic programming language.

This is a very elegant idea -- write assertions about heap shape using linear logic, and then check those assertions using a logic programming engine that traces the heap.

One thing this work reminds me is that I don't really understand the relationship between the way that they use the "with" connective (A & B) of linear logic and the way conjunction (A /\ B) is used in separation logic.

By neelk at 2007-03-10 18:50 | Software Engineering | other blogs | 7943 reads

Comment viewing options

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

IANAL

(I am not a logician) but someone may find "Linear Logic and Permutation Stacks" by Henry Baker interesting.

Josh

By J Storrs Hall at Mon, 2007-03-12 15:12 | login or register to post comments

I believe the answer to your

I believe the answer to your question is that in terms of the heap-shape semantics, they are "really" using separation logic. The entailment relation of linear logic is sound for this semantics, but (unlike bunched implications logic) not complete. The typical example is the failure of A & (B + C) |- (A & B) + (A & C) -- this is a mismatch with respect to the semantics, because it is always true that any heap described [by A and by either B or C] is described [by either A and B or by A and C]. So I believe the motivation for using linear logic in this paper (and the authors' prior work) is mostly practical, since there are more tools available (in particular the logic programming language LolliMon). It would be interesting to hear whether they have run into any problems with incompleteness.

By Noam at Mon, 2007-03-12 16:10 | login or register to post comments