<p>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 <em>sets of</em> heaps (or equivalently, predicates on heaps), and the separating conjunction $P \ast Q$ is defined as:</p>

<blockquote>
  <p>$$
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\}
$$</p>
</blockquote>

<p>So in the frame rule</p>

<blockquote>
  <p>$$
\frac{\{P\}c\{Q\}}{\{P\ast R\}c\{Q \ast R\}}
$$</p>
</blockquote>

<p>$R$ (and $P$ and $Q$) are not talking about specific heaps --- they
are <em>properties</em> 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>

<blockquote>
  <p>$$
\{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&lt;h_1\cdot h'; c\right&gt; \mapsto^\ast \left&lt;h_2\cdot h'; \mathsf{skip}\right&gt;
$$</p>
</blockquote>

<p>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 <em>specific</em> $h_2$ you get can
differ, for different choices of $h'$ --- what's being guaranteed is
that the <em>properties</em> $P$ and $Q$ will continue to hold under extension, not that you get exactly the same result heap.</p>

<p>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:</p>

<blockquote>
  <p>$$
\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\}}
$$</p>
</blockquote>

<p>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. </p>

<p>There's a discussion of this in the paper by Hoare et al, <a href="http://www.eecs.qmul.ac.uk/~rusmus/articles/LocalityBimonoid.pdf"><em>On Locality and the Exchange Law for Concurrent Processes</em></a>, where they show how to give a merged algebra of programs and assertions.</p>

CC BY-SA 3.0
2012-10-11T10:08:14.517Z
The definition for Hoare triples looks wrong: It should say the execution doesn't fault, it should allow for non-termination, it probably shouldn't preclude models that don't have safety monotonicity. (But, yes, I do agree it's perfectly reasonable to talk about "preservation-of-changes" for the reasons you explain.)
Radu GRIGore
CC BY-SA 3.0
2012-10-11T10:46:44.133Z
(1) I gave the semantics for total correctness triples, and so it asserts that the command completes safely -- I find that total correctness makes explaining the forall/exists character of pre and post-conditions easier to see. (2) This semantics of triples was actually invented (IIRC by Birkedal and Yang) to handle languages that don't have safety monotonicity in the language semantics, by building it into the meaning of triples. As a result, you can have non-monotonic constructs (e.g., queries about how big the heap is) in the language, while still having the frame rule for the Hoare logic.
Neel Krishnaswami
CC BY-SA 3.0
2012-10-11T11:05:33.077Z
(1) OK, but those triples are written differently. (2) I didn't know that. To rephrase what you said: without monotonicity you could lose the frame rule and keep using Hoare triples as usual, which is what I was getting at in the first comment, _but_ you could also strengthen the definition of a triple so that you get back the frame rule. (3) I don't see why it precludes faults. Do you assume $c$ is deterministic?
Radu GRIGore
CC BY-SA 3.0
2012-10-11T17:13:00.240Z
Thanks, Neel!  You're right, I was conflating the properties P and Q with specific heaps.  So, to sum up your comment: Q is preserved, but the particular heap that you get at the end could be a _different_ Q-satisfying heap than you were getting before.  Yes?
Lindsey Kuper
CC BY-SA 3.0
2012-10-12T14:25:31.690Z
@RaduGRIGore: yes, I was assuming that the language was deterministic, and this assumption will fail when we add concurrency. Nice catch!
Neel Krishnaswami
CC BY-SA 3.0
2012-10-12T14:26:10.783Z
@LindseyKuper: yes, exactly.
Neel Krishnaswami
CC BY-SA 3.0
2012-10-11T09:42:54.283Z
2012-10-11T09:42:54.283Z
Neel Krishnaswami
<p>While not 100% related, this has the flavor of contract idempotence. </p>

<p>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.</p>

<p>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 <em>idempotent</em> contracts.</p>

CC BY-SA 3.0
2012-10-11T02:06:21.140Z
Thanks for the comment.  Hm, interesting -- I wonder if anyone else reading this knows of contract papers that state frame properties.
Lindsey Kuper
CC BY-SA 3.0
2012-10-11T00:25:29.080Z
2012-10-11T00:25:29.080Z
kaosjester
<p>But this no-change-to-<code>q</code> property does not actually hold!</p>

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

<p><code>{y |-&gt; 3} x := alloc(0) {x |-&gt; 0 * y |-&gt; 3}</code></p>

<p>but, by the rule of consequence, I could change the postcondition to</p>

<p><code>{y |-&gt; 3} x := alloc(0) {(x |-&gt; 0 /\ x != y) * y |-&gt; 3}</code></p>

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

<p>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 <em>locality</em> for "actions", where an action is (the semantic representation of) a program.  Locality says that when you add in some frame heap, the <em>only</em> way that the original postcondition can be changed is by pruning some nondeterminism as above.  And, in fact, pruning only arises because of allocation.</p>

CC BY-SA 3.0
2012-10-11T04:12:25.117Z
Thanks for the example and for the reference!  Your example makes sense.

Is it fair to say, though, that `q` can only change to "`q`, and also..."?  And, furthermore, if allocation is the only thing that can prune the nondeterminism in the postcondition (which is a cool result in itself), then, if there's some part of the postcondition that is location-independent, then is that part of the postcondition guaranteed to stay the same?  Can we say that the postcondition stays the same up to alpha-renaming of locations?  (I have an example in mind, but maybe this is better explained via email.)
Lindsey Kuper
CC BY-SA 3.0
2012-10-11T15:09:20.677Z
Yes, `q` can only change to "`q`, and also..."  In other words, the postcondition can only become *stronger*: it will imply the original postcondition.  This is part of the definition of locality for actions.

It is not true, though, that the change to the postcondition is only tied to renaming.  In the example I gave, the extra fact that `x` and `y` are distinct is true regardless of the particular address chosen for `y`.  The example captures the *freshness* of allocation, which is invariant under renaming.
Aaron Turon
CC BY-SA 3.0
2012-10-11T02:09:17.727Z
2012-10-11T02:09:17.727Z
Aaron Turon
<p>A <em>frame rule</em>, like the one given below, captures the idea that, given a program <code>c</code> with precondition <code>p</code> that holds before it runs and postcondition <code>q</code> that holds afterward, some disjoint condition <code>r</code> should hold both before and after <code>c</code> runs.  (The <code>*</code> connective requires that its arguments be disjoint.)  Often, the pre- and postconditions are states of a heap, and <code>c</code> is an effectful program that modifies the heap in some way.</p>

<pre><code>    {p} c {q}
----------------- (where no free variable in r is modified by c)
{p * r} c {q * r}
</code></pre>

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

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

CC BY-SA 3.0
2012-10-11T01:44:04.063Z
One answer to my own question is in this paper: http://software.imdea.org/~gotsman/papers/interproc-sas06.pdf, in the sentence (emphasis mine) "If P ensures C’s footprint is allocated, then according to Frame, executing C in the presence of additional memory R **results in the same behavior**, and C does not touch the extra memory."  It's that "results in the same behavior" that I was looking for someone to point out, in addition to just "C does not touch the extra memory". (Thanks to @kaosjester for the link.)
Lindsey Kuper
CC BY-SA 3.0
2012-10-12T13:21:59.183Z
If you read through the soundness proofs of the frame rule and other rules of Separation Logic, you will discover that they are doing exactly what you are after, i.e., they talk about how the change from $p$ to $q$ is preserved.  Do pay attention to the locality and frame properties mentioned there.
Uday Reddy
<lo.logic><pl.programming-languages><program-logic>
Frame rule as a change-preserver?
Lindsey Kuper
# Frame rule as a change-preserver?

(Asked by: username_0 on 2012-10-10)

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.

**Tags:** lo.logic, pl.programming-languages, program-logic

> **Comments:**
> **username_0**: One answer to my own question is in this paper: http://software.imdea.org/~gotsman/papers/interproc-sas06.pdf, in the sentence (emphasis mine) "If P ensures C’s footprint is allocated, then according to Frame, executing C in the presence of additional memory R **results in the same behavior**, and C does not touch the extra memory."  It's that "results in the same behavior" that I was looking for someone to point out, in addition to just "C does not touch the extra memory". (Thanks to @username_4 for the link.)  
> **username_1**: If you read through the soundness proofs of the frame rule and other rules of Separation Logic, you will discover that they are doing exactly what you are after, i.e., they talk about how the change from $p$ to $q$ is preserved.  Do pay attention to the locality and frame properties mentioned there.  

---

## 3 answers

### Answer by username_5 on 2012-10-11. Score: 11 | Accepted answer

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.

> **Comments:**
> **username_0**: Thanks for the example and for the reference!  Your example makes sense.  Is it fair to say, though, that `q` can only change to "`q`, and also..."?  And, furthermore, if allocation is the only thing that can prune the nondeterminism in the postcondition (which is a cool result in itself), then, if there's some part of the postcondition that is location-independent, then is that part of the postcondition guaranteed to stay the same?  Can we say that the postcondition stays the same up to alpha-renaming of locations?  (I have an example in mind, but maybe this is better explained via email.)  
> **username_5**: Yes, `q` can only change to "`q`, and also..."  In other words, the postcondition can only become *stronger*: it will imply the original postcondition.  This is part of the definition of locality for actions.  It is not true, though, that the change to the postcondition is only tied to renaming.  In the example I gave, the extra fact that `x` and `y` are distinct is true regardless of the particular address chosen for `y`.  The example captures the *freshness* of allocation, which is invariant under renaming.  

---

### Answer by username_2 on 2012-10-11. Score: 11

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 \mapsto^\ast \left
> $$

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*](http://www.eecs.qmul.ac.uk/~rusmus/articles/LocalityBimonoid.pdf), where they show how to give a merged algebra of programs and assertions.

> **Comments:**
> **username_3**: The definition for Hoare triples looks wrong: It should say the execution doesn't fault, it should allow for non-termination, it probably shouldn't preclude models that don't have safety monotonicity. (But, yes, I do agree it's perfectly reasonable to talk about "preservation-of-changes" for the reasons you explain.)  
> **username_2**: (1) I gave the semantics for total correctness triples, and so it asserts that the command completes safely -- I find that total correctness makes explaining the forall/exists character of pre and post-conditions easier to see. (2) This semantics of triples was actually invented (IIRC by Birkedal and Yang) to handle languages that don't have safety monotonicity in the language semantics, by building it into the meaning of triples. As a result, you can have non-monotonic constructs (e.g., queries about how big the heap is) in the language, while still having the frame rule for the Hoare logic.  
> **username_3**: (1) OK, but those triples are written differently. (2) I didn't know that. To rephrase what you said: without monotonicity you could lose the frame rule and keep using Hoare triples as usual, which is what I was getting at in the first comment, _but_ you could also strengthen the definition of a triple so that you get back the frame rule. (3) I don't see why it precludes faults. Do you assume $c$ is deterministic?  
> **username_0**: Thanks, Neel!  You're right, I was conflating the properties P and Q with specific heaps.  So, to sum up your comment: Q is preserved, but the particular heap that you get at the end could be a _different_ Q-satisfying heap than you were getting before.  Yes?  
> **username_2**: @RaduGRIGore: yes, I was assuming that the language was deterministic, and this assumption will fail when we add concurrency. Nice catch!  
> **username_2**: @LindseyKuper: yes, exactly.  

---

### Answer by username_4 on 2012-10-11. Score: 2

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.

> **Comments:**
> **username_0**: Thanks for the comment.  Hm, interesting -- I wonder if anyone else reading this knows of contract papers that state frame properties.  

---

