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.