Frame rule as a change-preserver?
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.