Separation Logic (II) Acknowledgment:slides taken from Reynolds'mini-course CS 818A3
Separation Logic (II) Acknowledgment: slides taken from Reynolds’ mini-course CS 818A3
Specifications Partial correctness: ip}eta} Total correctness: [p]c[a] Note the spec now requires c does not abort
Specifications Partial correctness: Total correctness: Note the spec now requires c does not abort
Examples {emp}×:=cons(1,2){x-1,2} {x一1,2}y=[]{x一1,2∧y=1} {x→1,2Λy=1}[x+1]:=3{x-1,3∧y=1} {x→1,3∧y=1}dispose×{×+1-3∧y=1} {X→-*y一-} if y =x+1 then skip else if x=y+1 then x:=y else (dispose x;dispose y;x:=cons(1,2)) {x一-，-}
Examples
The Frame Rule (O'Hearn)(FR) p}crar p r}ciq r}, where no variable occurring free in r is modified by c
The Frame Rule (O’Hearn) (FR)
Why the Frame Rule is Sound We define: If,starting in the state s,h,no execution of a com- mand c aborts,then c is safe at s,h. If,starting in the state s,h,every execution of c termi- nates without aborting,then c must terminate normally at s,h. Then our programming language satisfies: Safety Monotonicity If hh and c is safe at s,h-h, then c is safe at s,h.If h c h and c must terminate normally at s,h-h,then c must terminate normally at s,h
Why the Frame Rule is Sound