Frame rule as a change-preserver?

Question

A frame rule, like the one given below, captures the idea that, given a program c with precondition p that holds before it runs and postcondition q that holds afterward, some disjoint condition r should hold both before and after c runs. (The * connective requires that its arguments be disjoint.) Often, the pre- and postconditions are states of a heap, and c is an effectful program that modifies the heap in some way.

    {p} c {q}
----------------- (where no free variable in r is modified by c)
{p * r} c {q * r}

Discussions of the frame rule that I've seen always seem to focus on how the disjoint part of the heap, r, is preserved. This enables "local reasoning": when reasoning about the effect that c has, we can disregard the r part of the heap and only concern ourselves with the part that actually changes. But another way to look at it is that the change from p to q is preserved, even though r is now sitting there. In other words, it's important that we end up with the postcondition {q * r}, rather than {q' * r} for some other q'.

So, my question is whether there's any treatment of the frame rule that discusses or makes use of the preservation-of-change-from-p-to-q thing.

Answer 1

But this no-change-to-q property does not actually hold!

Consider {emp} x := alloc(0) {x |-> 0}. Now, if I frame in y |-> 3, I get

{y |-> 3} x := alloc(0) {x |-> 0 * y |-> 3}

but, by the rule of consequence, I could change the postcondition to

{y |-> 3} x := alloc(0) {(x |-> 0 /\ x != y) * y |-> 3}

To make this more concrete, suppose y is the number 37. When I run the allocation command in a completely empty heap, it's possible that I will end up allocating address 37, so that x = 37. But, if I instead start with a heap containing a single cell at address y = 37, this outcome is no longer possible! Adding a frame to the precondition has pruned some of the nondeterminism in the postcondition.

The paper "Local action and abstract separation logic" (Calcagno, O'Hearn, and Yang) is all about understanding the frame rule from a deeper, semantic perspective. The key definition of the paper is locality for "actions", where an action is (the semantic representation of) a program. Locality says that when you add in some frame heap, the only way that the original postcondition can be changed is by pruning some nondeterminism as above. And, in fact, pruning only arises because of allocation.

Answer 2

First, there's a small misconception in the statement of your question, which is what Aaron was also getting at in his answer. Predicates in separation logic are sets of heaps (or equivalently, predicates on heaps), and the separating conjunction $P \ast Q$ is defined as:

$$ P \ast R \triangleq \{h_1 \cdot h_2 \;|\; h_1 \in P \;\wedge\; h_2 \in R \;\wedge\; \mathrm{dom}(h_1) \cap \mathrm{dom}(h_2) = \emptyset\} $$

So in the frame rule

$$ \frac{\{P\}c\{Q\}}{\{P\ast R\}c\{Q \ast R\}} $$

$R$ (and $P$ and $Q$) are not talking about specific heaps --- they are properties of heaps (since subsets and predicates are equivalent). The best way to understand what's going is by looking at the definition of what it means for a Hoare triple to hold:

$$ \{P\}c\{Q\} \triangleq \forall h_1 \in P.\; \forall h' \in \mathrm{Heap}\;\mbox{s.t.}\; h' \# h_1.\;\exists h_2 \in Q.\; \left<h_1\cdot h'; c\right> \mapsto^\ast \left<h_2\cdot h'; \mathsf{skip}\right> $$

This definition basically says that (1) if you run $c$ with any $h_1$ in $P$, then you'll finish in some final state $h_2$ in $Q$, and (2) if you add on any extra memory $h'$, that memory will be unchanged at the end of the run. But note that the specific $h_2$ you get can differ, for different choices of $h'$ --- what's being guaranteed is that the properties $P$ and $Q$ will continue to hold under extension, not that you get exactly the same result heap.

It's not too hard, but still worth working out, to see how this definition of Hoare triple implies that the frame rule holds. As you note, this is a kind of "preservation-of-changes" property, and it has a particularly vivid expression in the statement of the parallel composition rule in concurrent separation logic:

$$ \frac{\{P_1\}c_1\{Q_1\} \qquad \{P_2\}c_2\{Q_2\}}{\{P_1 \ast P_2\}c_1 || c_2 \{Q_1 \ast Q_2\}} $$

If $c_1$ and $c_2$ act on disjoint regions of memory, then each will not interfere with the properties of the other one's execution when they are run in parallel.

There's a discussion of this in the paper by Hoare et al, On Locality and the Exchange Law for Concurrent Processes, where they show how to give a merged algebra of programs and assertions.

Answer 3

While not 100% related, this has the flavor of contract idempotence.

If we think of {p} as a pre-condition on c and {q} as a post-condition on c, this idea of a frame rule would ensure that the pre- and post-conditions hold in every context of computation, not the simple case where nothing else exists.

That said, I cannot say that I've seen such a frame rule presented in any of the dozens of contract papers I have read. It's certainly a great idea, though, and requiring such a change may do a lot toward developing a reasonable, tangible understanding of idempotent contracts.