1.5.SPECIFICATIONS AND THEIR INFERENCE RULES > It is evident that such a program goes well beyond the discipline imposed by type systems for mutable data structures. In our new setting,the command-specific inference rules of Hoare logic remain sound,as do such structural rules as Strengthening Precedent p→q{q}c{r} {p}c{r}. Weakening Consequent {pc{g}q→r {p}c{r}. Existential Quantification(Ghost Variable Elimination) ip}efa} {3v.p}c{3u.q} where v is not free in c. ·Conjunction {p}c{q}{p}c{g2} {p}c{A2} ●Substitution {p}cfa} {p/8(c/o){g/ where 6 is the substitution ve1.....vn e h are the variables occurring free in p,c,or g,and,if v is modified by c,then e is a variable that does not occur free in any other (All of the inference rules presented in this section are the same for partial and total correctness.) An exception is what is sometimes called the "rule of constancy"[27, Section 3.3.5;28,Section 3.5]: ip}cfa} (unsound) ipAr}cfgnr}
1.5. SPECIFICATIONS AND THEIR INFERENCE RULES 17 It is evident that such a program goes well beyond the discipline imposed by type systems for mutable data structures. In our new setting, the command-specific inference rules of Hoare logic remain sound, as do such structural rules as • Strengthening Precedent p ⇒ q {q} c {r} {p} c {r}. • Weakening Consequent {p} c {q} q ⇒ r {p} c {r}. • Existential Quantification (Ghost Variable Elimination) {p} c {q} {∃v. p} c {∃v. q}, where v is not free in c. • Conjunction {p} c {q1} {p} c {q2} {p} c {q1 ∧ q2}. • Substitution {p} c {q} {p/δ} (c/δ) {q/δ}, where δ is the substitution v1 → e1, . . . , vn → en, v1, . . . , vn are the variables occurring free in p, c, or q, and, if vi is modified by c, then ei is a variable that does not occur free in any other ej . (All of the inference rules presented in this section are the same for partial and total correctness.) An exception is what is sometimes called the “rule of constancy” [27, Section 3.3.5; 28, Section 3.5]: {p} c {q} {p ∧ r} c {q ∧ r}, (unsound)
18 CHAPTER 1.AN OVERVIEW a "local"specification of c,involving only the variables actually used by that command,by adding arbitrary predicates about variables that are not modified by c and will therefore be preserved by its execution. Surprisingly,however,the rule of constancy becomes unsound when one moves nal Hoare logic to separation logic For example,the conclusion of the instance {x一-}冈：=4{x一4} {x-Ay一3}=4{x一4Ay3} is not valid,since its precondition does not preclude the case x=y,where aliasing will falsify y3 when the mutation command is executed. O'Hearn realized,however,that the ability to extend local specifications cat dceper level by ing s parating conjunction.In place of constancy,he proposed the frame rule ●Frame rule ip r}ciq r where no variable occurring free in r is modified by c. can extend a local specifcation,involvin only va. ables and heap cellsth at may actually be ed by c(which O'Hearn calls the footprint of c),by adding arbitrary predicates about variables and heap cells that are not modified or mutated by c.Thus,the frame rule is the key to "local reasoning"about the heap: To understand how a program works,it should be ssible for reasoning and specification to be confined to the cells that the program actually accesses.The value of any other cell will auto- matically remain unchanged [8]. In any valid specification p}},p must assert that the heap contains every cell in the foo print of c (except f ells that are freshly by c);"l is implication that every to be contained in the heap belongs to the footprint.The role of the frame rule is to infer from a local specification of a command the more global specification appropriate to the possibly larger footprint of an enclosing command
18 CHAPTER 1. AN OVERVIEW where no variable occurring free in r is modified by c. It has long been understood that this rule is vital for scalability, since it permits one to extend a “local” specification of c, involving only the variables actually used by that command, by adding arbitrary predicates about variables that are not modified by c and will therefore be preserved by its execution. Surprisingly, however, the rule of constancy becomes unsound when one moves from traditional Hoare logic to separation logic. For example, the conclusion of the instance {x 7→ −} [x] := 4 {x 7→ 4} {x 7→ − ∧ y 7→ 3} [x] := 4 {x 7→ 4 ∧ y 7→ 3} is not valid, since its precondition does not preclude the case x = y, where aliasing will falsify y 7→ 3 when the mutation command is executed. O’Hearn realized, however, that the ability to extend local specifications can be regained at a deeper level by using separating conjunction. In place of the rule of constancy, he proposed the frame rule: • Frame Rule {p} c {q} {p ∗ r} c {q ∗ r}, where no variable occurring free in r is modified by c. By using the frame rule, one can extend a local specification, involving only the variables and heap cells that may actually be used by c (which O’Hearn calls the footprint of c), by adding arbitrary predicates about variables and heap cells that are not modified or mutated by c. Thus, the frame rule is the key to “local reasoning” about the heap: To understand how a program works, it should be possible for reasoning and specification to be confined to the cells that the program actually accesses. The value of any other cell will automatically remain unchanged [8]. In any valid specification {p} c {q}, p must assert that the heap contains every cell in the footprint of c (except for cells that are freshly allocated by c); “locality” is the converse implication that every cell asserted to be contained in the heap belongs to the footprint. The role of the frame rule is to infer from a local specification of a command the more global specification appropriate to the possibly larger footprint of an enclosing command
1.5.SPECIFICATIONS AND THEIR INFERENCE RULES 19 Beyond the rules of Hoare logic and the frame rule,there are inference rules for each of the new heap-manipulating commands.Indeed,for each of these commands,we can give three kinds of rules:local,global,and backward-reasoning. For mutation,for example,the simplest rule is the local rule: 。Mutation(local) {e--}e=e{e-e'} which specifies the effect of mutation on the single cell being mutated.From this,one can use the frame rule to derive a global rule: ·Mutation(global) {(e--)*r}e=e{(ee)*r} which also specifies that anything in the heap beyond the cell being mutated anchanged by the mutation.(One can rederive the local rulefrom ng r to be e emp Beyond these forms,there is also: Mutation (backwards reasoning) {(e--)*(e一e)*p)}[g:=e{p} which is called a backward reasoning rule since,by substituting for p,one can find a precondition for any postcondition.5]. A similar development works for deallocation.except that the global form is itself suitable for backward reasoning Deallocation(local) fe-}dispose e [emp} Deallocation(global,backwards reasoning) {(e-）*r}dispose e{r} In the same way,one can give equivalent local and global rules for alloca- tion commands in the nonoverwriting case where the old value of the variable being modified plays no role.Here we abbreviate e,..n by
1.5. SPECIFICATIONS AND THEIR INFERENCE RULES 19 Beyond the rules of Hoare logic and the frame rule, there are inference rules for each of the new heap-manipulating commands. Indeed, for each of these commands, we can give three kinds of rules: local, global, and backward-reasoning. For mutation, for example, the simplest rule is the local rule: • Mutation (local) {e 7→ −} [e] := e 0 {e 7→ e 0}, which specifies the effect of mutation on the single cell being mutated. From this, one can use the frame rule to derive a global rule: • Mutation (global) {(e 7→ −) ∗ r} [e] := e 0 {(e 7→ e 0 ) ∗ r}, which also specifies that anything in the heap beyond the cell being mutated is left unchanged by the mutation. (One can rederive the local rule from the global one by taking r to be emp.) Beyond these forms, there is also: • Mutation (backwards reasoning) {(e 7→ −) ∗ ((e 7→ e 0 ) −∗ p)} [e] := e 0 {p}, which is called a backward reasoning rule since, by substituting for p, one can find a precondition for any postcondition. [5]. A similar development works for deallocation, except that the global form is itself suitable for backward reasoning: • Deallocation (local) {e 7→ −} dispose e {emp}. • Deallocation (global, backwards reasoning) {(e 7→ −) ∗ r} dispose e {r}. In the same way, one can give equivalent local and global rules for allocation commands in the nonoverwriting case where the old value of the variable being modified plays no role. Here we abbreviate e1, . . . , en by e
30 CHAPTER 1.AN OVERVIEW Allocation(nonoverwriting,local) {emp}v:=cons(e{v→e} where v is not free in e. .Allocation(nonoverwriting,global) {r}v:=cons(e){(v)*r}, where u is not free in e or r. Of course.we also need more general rules for allocation commands v:= ooringothprdition backward and rules for lookup. all of thes are more compicated than those given above (largely because most of them contain quantifiers),we postpone them to Section 3.7 (where we will also show that the different forms of rules for each command are interderivable). As a simple illustration of separation logic,the following is an anno- tated specification of the command(1.5)that tries to glue together adjacent records: {x一-*y一-} if y=x+1 then {x-,-} skip else if x=y+1 then {y一-，-} x:=y else ({x一-*y→-} disposex; {y--} dispose y; {emp} ×=cons(1,2) {x一-，-}
20 CHAPTER 1. AN OVERVIEW • Allocation (nonoverwriting, local) {emp} v := cons(e) {v 7→ e}, where v is not free in e. • Allocation (nonoverwriting, global) {r} v := cons(e) {(v 7→ e) ∗ r}, where v is not free in e or r. Of course, we also need more general rules for allocation commands v := cons(e), where v occurs in e or the precondition, as well as a backwardreasoning rule for allocation, and rules for lookup. Since all of these rules are more complicated than those given above (largely because most of them contain quantifiers), we postpone them to Section 3.7 (where we will also show that the different forms of rules for each command are interderivable). As a simple illustration of separation logic, the following is an annotated specification of the command (1.5) that tries to glue together adjacent records: {x 7→ − ∗ y 7→ −} if y = x + 1 then {x 7→ −, −} skip else if x = y + 1 then {y 7→ −, −} x := y else ({x 7→ − ∗ y 7→ −} dispose x ; {y 7→ −} dispose y ; {emp} x := cons(1, 2)) {x 7→ −, −}
1.6.LISTS 3 We will make the concept of an annotated specification-as a user-friendly form for presenting proof of specifications-rigorous in Sections 3.3 and 3.6. For the present,one can think of the intermediate assertions as comments that must be true whenever control passes through them(assuming the initial assertion is true when the program begins execution),and that must also ensure the correct functioning of the rest of the program being exe ecuted A second example describes a command that uses allocation and mutation to construct a two-element cyclic structure containing relative addresses: {emp} x:=cons(a,a): xa,a y:=cons(b,b) {x一a,a)*(y一b,b)} {x一a,-）*(y一b.-)} x+1=y-x; {(x一a,y-x)*(y一b,-)月 y+1刂=×-y; {(xa,y-x)*(yb,x-y)} {30.(x一a,o)*(x+0一b,-o)} 1.6 Lists To specify a program adequately,it is usually necessary to describe more than the form of its structures or the sharing patterns between them;one must relate the states of the program to the abstract values that they denote.For instance,to specify the list-reversal program in Section 1.1,it would hardly be enough to say that "If i is a list before execution,then j will be a list afterwards"One needs tosay that "list representing the sequen before e exe ution has the refcto oterwardswill be a list representing the sequencd To do so in general,it is necessary to define the set of abstract values (sequences,in this case),along with their primitive operations,and then to define predicates on the abstract values by structural induction.Since these
1.6. LISTS 21 We will make the concept of an annotated specification — as a user-friendly form for presenting proof of specifications — rigorous in Sections 3.3 and 3.6. For the present, one can think of the intermediate assertions as comments that must be true whenever control passes through them (assuming the initial assertion is true when the program begins execution), and that must also ensure the correct functioning of the rest of the program being executed. A second example describes a command that uses allocation and mutation to construct a two-element cyclic structure containing relative addresses: {emp} x := cons(a, a) ; {x 7→ a, a} y := cons(b, b) ; {(x 7→ a, a) ∗ (y 7→ b, b)} {(x 7→ a, −) ∗ (y 7→ b, −)} [x + 1] := y − x ; {(x 7→ a, y − x) ∗ (y 7→ b, −)} [y + 1] := x − y ; {(x 7→ a, y − x) ∗ (y 7→ b, x − y)} {∃o. (x 7→ a, o) ∗ (x + o 7→ b, − o)}. 1.6 Lists To specify a program adequately, it is usually necessary to describe more than the form of its structures or the sharing patterns between them; one must relate the states of the program to the abstract values that they denote. For instance, to specify the list-reversal program in Section 1.1, it would hardly be enough to say that “If i is a list before execution, then j will be a list afterwards”. One needs to say that “If i is a list representing the sequence α before execution, then afterwards j will be a list representing the sequence that is the reflection of α.” To do so in general, it is necessary to define the set of abstract values (sequences, in this case), along with their primitive operations, and then to define predicates on the abstract values by structural induction. Since these