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.

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.