Commit 2a4baa1d authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Rename some rules : pvs -> vup.

parent 06b05439
...@@ -230,10 +230,10 @@ The following rules can all be derived inside the DC logic: ...@@ -230,10 +230,10 @@ The following rules can all be derived inside the DC logic:
{\mask_1 \subseteq \mask_2 \and \vctx,\var:\textlog{val}\mid\prop \proves \propB} {\mask_1 \subseteq \mask_2 \and \vctx,\var:\textlog{val}\mid\prop \proves \propB}
{\vctx\mid\wpre\expr[\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\mask_2]{\Ret\var.\propB}} {\vctx\mid\wpre\expr[\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\mask_2]{\Ret\var.\propB}}
\infer[pvs-wp] \infer[vup-wp]
{}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}} {}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
\infer[wp-pvs] \infer[wp-vup]
{}{\wpre\expr[\mask]{\Ret\var.\pvs[\mask] \prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}} {}{\wpre\expr[\mask]{\Ret\var.\pvs[\mask] \prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
\infer[wp-atomic] \infer[wp-atomic]
......
...@@ -87,6 +87,7 @@ Section proof. ...@@ -87,6 +87,7 @@ Section proof.
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose". rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame. wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed. Qed.
End proof. End proof.
Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ := Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
......
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