Commit 98f58353 authored by Ralf Jung's avatar Ralf Jung

docs: new frame-step rules

parent 92e6ef6b
...@@ -176,8 +176,8 @@ The following rules can be derived for Hoare triples. ...@@ -176,8 +176,8 @@ The following rules can be derived for Hoare triples.
{\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask]} {\hoare{\prop * \propC}{\expr}{\Ret\val. \propB * \propC}[\mask]}
\and \and
\inferH{Ht-frame-step} \inferH{Ht-frame-step}
{\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \toval(\expr) = \bot} {\hoare{\prop}{\expr}{\Ret\val. \propB}[\mask] \and \toval(\expr) = \bot \and \mask_2 \subseteq \mask_2 \\\\ \propC_1 \vs[\mask_1][\mask_2] \later\propC_2 \and \propC_2 \vs[\mask_2][\mask_1] \propC_3}
{\hoare{\prop * \later\propC}{\expr}{\Ret\val. \propB * \propC}[\mask]} {\hoare{\prop * \propC_1}{\expr}{\Ret\val. \propB * \propC_3}[\mask \uplus \mask_1]}
\and \and
\inferH{Ht-atomic} \inferH{Ht-atomic}
{\prop \vs[\mask \uplus \mask'][\mask] \prop' \\ {\prop \vs[\mask \uplus \mask'][\mask] \prop' \\
......
...@@ -584,8 +584,8 @@ This is entirely standard. ...@@ -584,8 +584,8 @@ This is entirely standard.
{}{\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}} {}{\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}}
\infer[wp-frame-step] \infer[wp-frame-step]
{\toval(\expr) = \bot} {\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1}
{\later\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}} {\wpre\expr[\mask]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2]\later\pvs[\mask_2][\mask_1]\propB \proves \wpre\expr[\mask \uplus \mask_1]{\Ret\var.\propB*\prop}}
\infer[wp-bind] \infer[wp-bind]
{\text{$\lctx$ is a context}} {\text{$\lctx$ is a context}}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment