hw2: correct while semantics

2026-03-06 00:52:02 -08:00
parent d3479a5b88
commit 022f9ca2fc
2 changed files with 3 additions and 2 deletions
--- a/hw2/while-semantics.tex
+++ b/hw2/while-semantics.tex
@@ -150,9 +150,10 @@ such as sequencing operations ($e_1;e_2$).
 }
 \bsrule{B-WhileTrue}{
  \bstep{e_1}{\sigma}{\true}{\sigma'} \\
-  \bstep{e_2}{\sigma'}{v}{\sigma''}
+  \bstep{e_2}{\sigma'}{v_1}{\sigma''} \\
+  \bstep{\whilee{e_1}{e_2}}{\sigma''}{v}{\sigma'''}
 }{
-  \bstep{\whilee{e_1}{e_2}}{\sigma}{v}{\sigma''}
+  \bstep{\whilee{e_1}{e_2}}{\sigma}{v}{\sigma'''}
 }
 \bsrule{B-WhileFalse}{
  \bstep{e_1}{\sigma}{\false}{\sigma'}