QCP Tutorials Memory and Assertions

Shanghai Jiao Tong University Cao Qinxiang Research Group

T2-2 · Memory and Assertions

Common Assertion Forms and Properties of Separating Conjunction

As we have seen in the preceding examples, the QCP assertion language supports the logical connectives && and *. The former denotes the usual logical "and", while the latter is the separating conjunction. Specifically, "P * Q" states that the current memory can be divided into two disjoint parts, one satisfying P and the other satisfying Q. We can use these connectives to combine multiple clauses and thereby express more complex concepts.

Suppose p is a logical variable whose value is a memory address. Then

exists v, v >= 0 && store_int(p, v)

states that a non-negative number is stored at address p.

Suppose p and q are both logical variables whose values are memory addresses. Then

exists v, store_int(p, v) * store_int(q, v)

states that p and q are different addresses, but the same value is stored at both addresses.

Of course, we can also write more complex assertions:

exists v, store_int(p, v) * store_int(q, v)

This states that p and q are different addresses, but the same non-negative number is stored at both addresses.

As introduced earlier, the separating conjunction ("*") is commutative and associative. That is:

P * Q       <----> Q * P
P * (Q * R) <----> (P * Q) * R

It also has the following two important properties:

  • Associativity between && and *: If P is a proposition that does not involve memory (such as a comparison v >= 0), then (P && Q) * R <----> P && (Q ** R). The left-hand side of this equivalence says that memory can be divided into two parts, one satisfying P && Q and the other satisfying R. Since P is a memory-independent proposition, this is equivalent to saying that P holds and that memory can be divided into two parts satisfying Q and R respectively -- which is exactly the property described by the right-hand side. Because of this property, when the P connected by && is a memory-independent expression, a formula like P && Q * R can be written without parentheses to indicate the binding order between && and *.

  • Associativity between exists and *: (exists x, P(x)) * Q <----> exists x, (P(x) * Q). Because of this property, we can always hoist exists from within a separating conjunction clause to the outermost level.