Why the Frame Rule is Sound The Frame Property If h Ch,cis safe at s,h-h,and some execution of c starting at s,h terminates normally in the state s',h', s,h-五.C—s,h2i c safe s',h' then hh'and some execution of c starting at s,h-h, terminates normally in the state s',h'-h
Why the Frame Rule is Sound
Why the Frame Rule is Sound s,h-i.c-s,h2一n csafe s,h' s,h-hi.s,h2.h C s,h-.-.-s/.h
Why the Frame Rule is Sound
Inference Rules for Mutation The local form(MUL): {e--}[e]:=e'{e-e}. The global form(MUG): {(e--)*r}[e]:=e'{(e-e)*r}. The backward-reasoning form(MUBR): {(e一-)*(e一e)-*p)}[e]:=e'{p}. One rule implies another
Inference Rules for Mutation One rule implies another
The local form(MUL): {e→-}[e]:=e'{e→ye The global form (MUG): {(e一-)*r}[e]=e'{(ee)*r}. One can derive(MUG)from(MUL)by using the frame rule: {(e→-)*r} {e→-} [e]:=e r {e-e) {(e→e)*r}
The local form (MUL): {e→-}[e]:=e'{e→e'} The global form(MUG): {(e--)*r}[e]:=e'{(e-e)*r}. To go in the opposite direction it is only necessary to take r to be emp: {e→-} {(e--)*emp} [e]:=e {(e一e)*emp} {e-e'}