Show description

T substitution principle. Rule Subst is a standard Sample True and False Entailments x=y x → x ∗ ls(x , y) ls(x, y) x→x ∗y →y x→x ∗x→y x=x x → x ∗ ls(x , y) ∗ y → z ls(x, y) ∗ y → z ls(x, x ) ∗ ls(y, y ) x = y The three examples on the left illustrate the anti-aliasing or separating properties of ∗, where the two on the right illustrate issues to be taken into account in rules for appending onto the end of list segments (a point which is essential in completeness considerations [2]). Appending a cell to the head of a list is always valid, as long as we make sure the end-points are distinct: (z = x) ∧ x → y ∗ ls(y, z) ls(x, z), whereas appending a cell to the tail of a list generally is not valid.

Cycles can be expressed with compound formulae. For instance, ls(y, x) ∗ ls(x, y) describes two acyclic non-empty linked lists which together form a cycle: this is the kind of structure sometimes used in cyclic buffer programs. As always in program analysis, what cannot be said is important for allowing efficient algorithms for consistency and entailment checking. General separation logic, which allows ∗ and its adjoint −∗ to be combined with all boolean connectives, is undecidable even at the propositional level [4].

The size of any candidate X is O(n2 ) is quadratic in the size of A and B. 3 below), each candidate X can be checked in polynomial time as to whether it is a solution or not. 4 below) guarantees the completeness of our procedure. The gist of this argument is that we can check a candidate solution in polynomial time, and only polynomial-sized solutions need be considered (by Interpolation). The entailment procedure we use to check solutions relies essentially on our use of necessarily non-empty list segments (as in [13]).