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