22 CHAPTER 1.AN OVERVIEW kinds of definition are standard,we will treat the than the novel aspects of our logic. Sequences and their primitive operations are an easy first example since they are a standard and well-understood mathematical concept,so that we ean omit their definition.To denote the pr erations write e for the empty sequence,a for the the reflection of a,and a;for the ith component of a. The simplest list structure for representing sequences is the singly-linked list.To describe this representation,we write list ai when i is a list repre- senting the sequence a: 但8园 It is straightforward to define this predicate by induction on the structure of a: list ci emp Ai=nil list(aa)i些j.i→a,j*listaj ents an empty sequence list a i→(i=nil÷a=e) Then the following is an annotated specification of the program for reversing
22 CHAPTER 1. AN OVERVIEW kinds of definition are standard, we will treat them less formally than the novel aspects of our logic. Sequences and their primitive operations are an easy first example since they are a standard and well-understood mathematical concept, so that we can omit their definition. To denote the primitive operations, we write for the empty sequence, α · β for the composition of α followed by β, α † for the reflection of α, and αi for the ith component of α. The simplest list structure for representing sequences is the singly-linked list. To describe this representation, we write list α i when i is a list representing the sequence α: ◦ i ✲ α1 ◦ α2 nil ✯ ✯ αn · · · ✯ It is straightforward to define this predicate by induction on the structure of α: list i def = emp ∧ i = nil list(a·α)i def = ∃j. i 7→ a, j ∗ list α j (where denotes the empty sequence and α·β denotes the concatenation of α followed by β), and to derive a test whether the list represents an empty sequence: list α i ⇒ (i = nil ⇔ α = ). Then the following is an annotated specification of the program for reversing
1.7.TREES AND DAGS 子 a list: {list ooi} {list aoi+(emp A nilnil)} j:=nil; flist aoi (emp Aj=nil)} {list aoi listej} {a,B.(list a i list Bj)A ao at.B} while i≠nil do （{3a,a,3.(ist(aa)i*list3j)∧a话=(aa)i.3} {3a,a,6,k.(0→a,k*list ak*list3j)∧a话=(aa)t} k=i+1刂； {a,a,B.(ia,k list ak list Bj)Aao=(a-a)t.B} 0+1=j {3a,a,B.(i一a,j*list ak*list Bj)Λa。=(aa)f.3} {a,a,B.(list ak list (a-B)i)Aao=at.a.B} {目a,月.(listak*list3i)Aa=at.3} j:=i;i:=k {a,B.(list ai*list Bj)a=at.3)) {3a,B.list BjA ao at.Ba=e} flist anj Within the assertions here,Greek letters are used as variables denoting se- have extended the state to map Grck aribi as sans serif variables into integers. 1.7 Trees and Dags When we move from list to tree structures,the possible patterns of sharing within the structures become richer. At the outset,we face a problem of nomenclature:Words such as "tree" and "graph"are often used to describe a variety of abstract structures,as
1.7. TREES AND DAGS 23 a list: {list α0 i} {list α0 i ∗ (emp ∧ nil = nil)} j := nil ; {list α0 i ∗ (emp ∧ j = nil)} {list α0 i ∗ list j} {∃α, β. (list α i ∗ list β j) ∧ α † 0 = α † ·β} while i 6= nil do ({∃a, α, β. (list(a·α)i ∗ list β j) ∧ α † 0 = (a·α) † ·β} {∃a, α, β, k. (i 7→ a, k ∗ list α k ∗ list β j) ∧ α † 0 = (a·α) † ·β} k := [i + 1] ; {∃a, α, β. (i 7→ a, k ∗ list α k ∗ list β j) ∧ α † 0 = (a·α) † ·β} [i + 1] := j ; {∃a, α, β. (i 7→ a, j ∗ list α k ∗ list β j) ∧ α † 0 = (a·α) † ·β} {∃a, α, β. (list α k ∗ list(a·β)i) ∧ α † 0 = α † ·a·β} {∃α, β. (list α k ∗ list β i) ∧ α † 0 = α † ·β} j := i ; i := k {∃α, β. (list α i ∗ list β j) ∧ α † 0 = α † ·β}) {∃α, β. list β j ∧ α † 0 = α † ·β ∧ α = } {list α † 0 j} Within the assertions here, Greek letters are used as variables denoting sequences. More formally, we have extended the state to map Greek variables into sequences as well as sans serif variables into integers. 1.7 Trees and Dags When we move from list to tree structures, the possible patterns of sharing within the structures become richer. At the outset, we face a problem of nomenclature: Words such as “tree” and “graph” are often used to describe a variety of abstract structures, as
24 CHAPTER 1.AN OVERVIEW well as particula community.The set S-exps of these values is the least set such that re S-exps iff r e Atoms or T=(n T2)where T,T2 e S-exps (Of course,this is just a particular,and very simple,initial algebra-as is "sequence".We could take carriers of any lawless many-sorted initial algebra to be our abstract data,but this would complicate our exposition naintain the distinction between abstract values and their representations Thus,we will call abstract values"S-expressions" while calling representations without sharing "trees",and representations with sharing but no cycles“dags”(for“directed acyclic graphs'"). We write treer(i)(or dag r(i))to indicate that i is the root of a tree (or dag)representing the S-expression r.Both predicates are defined by induction on the structure of: tree a(i)iff empAi=a tree(·T2)(i)i证]i1,i2.i一i1,i2*tree T(ii)*tree T2(i2) dag a(i)iff i=a dag(m·2)()证k妇i1,i2.i一i1,2*(dagT(i)Adag2(i2)》 (In Sections 5.1 and 5.2,we will see that treer(i)is a precise assertion,so that it describes a heap containing a tree-representation of r and nothing else,while dag(i)is an intuitionistic assertion,describing sa heap that may contain extra a space as well as a tree-representation of r.) 1.8 Arrays and the Iterated Separating Con- junction It is straightforward to extend ou programming language to include heap allocated one-dimensional arrays,by introducing an allocation command where the number of consecutive heap cells to be allocated is specified by an operand.It is simplest to leave the initial values of these cells indetermi- nate
24 CHAPTER 1. AN OVERVIEW well as particular ways of representing such structures. Here we will focus on a particular kind of abstract value called an “S-expression” in the LISP community. The set S-exps of these values is the least set such that τ ∈ S-exps iff τ ∈ Atoms or τ = (τ1 · τ2) where τ1, τ2 ∈ S-exps. (Of course, this is just a particular, and very simple, initial algebra — as is “sequence”. We could take carriers of any lawless many-sorted initial algebra to be our abstract data, but this would complicate our exposition while adding little of interest.) For clarity, it is vital to maintain the distinction between abstract values and their representations. Thus, we will call abstract values “S-expressions”, while calling representations without sharing “trees”, and representations with sharing but no cycles “dags” (for “directed acyclic graphs”). We write tree τ (i) (or dag τ (i)) to indicate that i is the root of a tree (or dag) representing the S-expression τ . Both predicates are defined by induction on the structure of τ : tree a (i) iff emp ∧ i = a tree (τ1 · τ2) (i) iff ∃i1, i2. i 7→ i1, i2 ∗ tree τ1 (i1) ∗ tree τ2 (i2) dag a (i) iff i = a dag (τ1 · τ2) (i) iff k∃i1, i2. i 7→ i1, i2 ∗ (dag τ1 (i1) ∧ dag τ2 (i2)). (In Sections 5.1 and 5.2, we will see that tree τ (i) is a precise assertion, so that it describes a heap containing a tree-representation of τ and nothing else, while dag τ (i) is an intuitionistic assertion, describing sa heap that may contain extra space as well as a tree-representation of τ .) 1.8 Arrays and the Iterated Separating Conjunction It is straightforward to extend our programming language to include heapallocated one-dimensional arrays, by introducing an allocation command where the number of consecutive heap cells to be allocated is specified by an operand. It is simplest to leave the initial values of these cells indeterminate
1.8.ARRAYS AND THE ITERATED SEPARATING CONJUNCTION25 We will use the syntax (comm):=…|var）:=allocate(exp） where v:=allocate e will be a command that allocates e consecutive locations and makes the first of these locations the value of the variable v.For instance: Store x:3,y:4 Heap:empty x:=allocate y Store:x:37,y:4 Heap:37:-,38:-,39:-,40: To describe such arrays,it is helpful to extend the concept of separating conjunction to a construct that iterates over a finite contiguous set of integers. We use the syntax (assert)=…|⊙=ep(assert) Roughly speaking,p bears the same relation to that bears to A.More precisely,let be the contiguous set of integers between the values of e and e'.Then Op(v)is true iff the heap can be partitioned into a family of disjoint subheaps,indexed by I,such that p(v) is true for the uth subheap. Then array allocation is described by the following inference rule: rv:=allocatee(oi-)*r where v does not occur free in r or e. A simple illustration of the iterated separating conjunction is the use of an array as a cyclic buffer.We assume that an n-element array has been allocated at address,e.g.by =allocaten,and we use the ariables m number of active elements dress of first active element j address of first inactive element Then when the buffer contains a sequence a,it should satisfy the assertion 0≤m≤nAI≤i<l+nAI≤j<I+nA j=imAm=#aA (⊙i⊕k一k+1)*(⊙=0-1j⊕k一-》 where r⊕y=x+y modulo n,andl≤x⊕y<|+n
1.8. ARRAYS AND THE ITERATED SEPARATING CONJUNCTION25 We will use the syntax hcommi ::= · · · | hvari := allocate hexpi where v:=allocate e will be a command that allocates e consecutive locations and makes the first of these locations the value of the variable v. For instance: Store : x: 3, y: 4 Heap : empty x := allocate y ⇓ Store : x: 37, y: 4 Heap : 37: −, 38: −, 39: −, 40: − To describe such arrays, it is helpful to extend the concept of separating conjunction to a construct that iterates over a finite contiguous set of integers. We use the syntax hasserti ::= · · · | Jhexpi hvari=hexpi hasserti Roughly speaking, Je 0 v=e p bears the same relation to ∗ that ∀ e 0 v=e p bears to ∧. More precisely, let I be the contiguous set { v | e ≤ v ≤ e 0 } of integers between the values of e and e 0 . Then Je 0 v=e p(v) is true iff the heap can be partitioned into a family of disjoint subheaps, indexed by I, such that p(v) is true for the vth subheap. Then array allocation is described by the following inference rule: {r} v := allocate e {( Jv+e−1 i=v i 7→ −) ∗ r}, where v does not occur free in r or e. A simple illustration of the iterated separating conjunction is the use of an array as a cyclic buffer. We assume that an n-element array has been allocated at address l, e.g., by l := allocate n, and we use the variables m number of active elements i address of first active element j address of first inactive element. Then when the buffer contains a sequence α, it should satisfy the assertion 0 ≤ m ≤ n ∧ l ≤ i < l + n ∧ l ≤ j < l + n ∧ j = i ⊕ m ∧ m = #α ∧ ((Jm−1 k=0 i ⊕ k 7→ αk+1) ∗ ( Jn−m−1 k=0 j ⊕ k 7→ −)), where x ⊕ y = x + y modulo n, and l ≤ x ⊕ y < l + n
CHAPTER 1.AN OVERVIEW 1.9 Proving the Schorr-Waite Algorithm One of the most ambitious applications of separation logic has been Yang's proof of the norr-Wai algorithm for mark g structures that contain shar- ing and cycles [12,10.This proof uses the older form of classical separation logic 5]in which address arithmetic is forbidden and the heap maps ad- dresses into multifield records-each containing,in this case,two address fields and two boolean fields. Since addresses refer to entire records with identical number and types of fields,it is easy to assert that the record at x has been allocated: allocated(x),,-,-, that all records in the heap are marked: markedR e Vx.allocated(x)x,-,-,true that x is not a dangling address: noDangling(x)(x=nil)vallocated(x). or that no record in the heap contains a dangling address: noDanglingR e Vx,I,r.(xr,-,- noDangling(I)A noDangling(r). The heap described by the main invariant of the program is the footprint of the entire algorithm,which is exactly the structure that is reachable from the address root.The invariant itself is: noDanglingR A noDangling(t)A noDangling(p)A (listMarkedNodesR(stack,p)* (restoredListR(stack,t)-spansR(STree,root)))A (markedR (unmarkedRA(Vx.allocated(x) (reach(t,x)VreachRightChildlnList(stack,x) At the point in the computation described by this invariant,the value of the variable t indicates the current subheap that is about to be scanned.At the
26 CHAPTER 1. AN OVERVIEW 1.9 Proving the Schorr-Waite Algorithm One of the most ambitious applications of separation logic has been Yang’s proof of the Schorr-Waite algorithm for marking structures that contain sharing and cycles [12, 10]. This proof uses the older form of classical separation logic [5] in which address arithmetic is forbidden and the heap maps addresses into multifield records — each containing, in this case, two address fields and two boolean fields. Since addresses refer to entire records with identical number and types of fields, it is easy to assert that the record at x has been allocated: allocated(x) def = x ,→ −, −, −, −, that all records in the heap are marked: markedR def = ∀x. allocated(x) ⇒ x ,→ −, −, −, true, that x is not a dangling address: noDangling(x) def = (x = nil) ∨ allocated(x), or that no record in the heap contains a dangling address: noDanglingR def = ∀x, l, r. (x ,→ l, r, −, −) ⇒ noDangling(l) ∧ noDangling(r). The heap described by the main invariant of the program is the footprint of the entire algorithm, which is exactly the structure that is reachable from the address root. The invariant itself is: noDanglingR ∧ noDangling(t) ∧ noDangling(p) ∧ (listMarkedNodesR(stack, p) ∗ (restoredListR(stack,t) −∗ spansR(STree, root))) ∧ (markedR ∗ (unmarkedR ∧ (∀x. allocated(x) ⇒ (reach(t, x) ∨ reachRightChildInList(stack, x))))). At the point in the computation described by this invariant, the value of the variable t indicates the current subheap that is about to be scanned. At the