Frame rule as a change-preserver? 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.
But this no-change-to-q property does not actually hold!

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

{y |-&gt; 3} x := alloc(0) {x |-&gt; 0 * y |-&gt; 3}

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

{y |-&gt; 3} x := alloc(0) {(x |-&gt; 0 /\ x != y) * y |-&gt; 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.