南京大学：《程序设计语言的形式语义》课程教学资源（课件讲稿）Separation Logic（1/3）

Separation Logic Acknowledgment:slides taken from Reynolds'mini-course CS 818A3

Separation Logic Acknowledgment: slides taken from Reynolds’ mini-course CS 818A3

Extending Imp with Memory Accesses Syntax: (comm)c::=... |x:=[e I [e]:=e' x cons(e1,e2) I dispose(e) Program States (store)s∈Var→Z (heap)h∈ N-fin Z (state)σ：= (s,h)

Extending Imp with Memory Accesses

Store:x:3,y:4 Heap:empty Allocation x:=cons(1,2); ↓ Store:x:37,y:4 Heap:37:1,38:2 Lookup y:=[x; 业 Store x:37,y:1 Heap:37:1,38:2 Mutation [x+1]:=3; 业 Store: x:37,y:1 Heap 37:1,38:3 Deallocation dispose(x+1) ↓ Store x:37,y:1 Heap:37:1 Note that expressions depend only on the store

Note that expressions depend only on the store

Memory Faults Store:x:3,y:4 Heap:empty Allocation x:cons(1,2); 业 Store x:37,y:4 Heap:37:1,38:2 Lookup y:=[x] 业 Store:x:37,y:1 Heap:37:1,38:2 Mutation [x+2]:=3; 业 abort Faults can also be caused by out-of-range lookup or dealloca- tion

Operational Semantics h(Iellintexps)=n (x :[e],(s,h))(skip,(s(x n),h)) lellintexp s dom(h) (x:=[e],(s,h)→abort [ellintexps=e ee dom(h) ([e]:=e',(s,h))(skip,(s,hie Ie'llintexp s))) [ellintexps年dom(h) ([e:=e',(s,h)→abort lle1 llintexps=n1 Ie2llintexps n2 (e,+1]n dom(h)=0 (x:=cons(e1,e2),(s,h))(skip,(s(xe),hie n,+1 n2)))

Operational Semantics

Assertions Standard predicate logic assertions,plus ·emp (empty heap) The heap is empty. ●e→e (singleton heap) The heap contains one cell,at address e with contents e'. ●p1*P2 (separating conjunction) The heap can be split into two disjoint parts such that p1 holds for one part and p2 holds for the other. ·P1-*P2 (separating implication) If the heap is extended with a disjoint part in which p1 holds, then p2 holds for the extended heap

Assertions Standard predicate logic assertions, plus

Some Abbreviations e、 def a.e where a'not free in e ee der ee*true def e→e1,..,ene→e1*.·*e+n-1→en def e→e1,.·,em dere一e1*…*e十n-1一en ife一e1,.,en*true

Examples of Separating Conjunction 1.x3,y asserts that x points to an adjacent 3 pair of cells containing 3 and y. y 2.y→3，x asserts that y points to an adjacent y pair of cells containing 3 and x. 3.x一3，y*y一3，x asserts that situations (1)and(2)hold for separate parts of the heap

4.x一3，y∧y→3，x asserts that situations (1)and(2)hold for the same heap,which can only happen if the values of x and y are the same. 5.x一3，y∧y→3，x asserts that either (3)or (4)may hold,and that the heap may contain additional cells

An Example of Separating Implication Suppose p holds for Rest Store:x:a,..· 3 of Heap:a:3,a+1:4,. 4 Heap Then (x3,4)-*p holds for Rest Store x:a,.. X一→ of Heap:.· Heap and x1,2 ((x3,4)-*p)holds for Rest Store:x:a,.. of Heap:a:1,a+1:2,.. Heap