Tag Info

13

You probably want Manna, Pnueli, Axiomatic Approach to Total Correctness of Programs, 1973

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\...

11

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, ...

7

I recently finished writing a survey of Ownership Types and found very little that discusses the relationship between the two topics. The three closest papers I came across are the following, which curiously come from the same conference: Yang Zhao and John Boyland. A fundamental permission interpretation for ownership types. In Second IEEE/IFIP ...

4

There is also a three-page paper by Turing that uses ranking functions to give a correctness proof. His paper is completely readable by modern standards and extremely prescient. Checking a large routine, Alan Turing, Report of a Conference on High Speed Automatic Calculating Machines, pp.67-69, 1949.

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

Only top voted, non community-wiki answers of a minimum length are eligible