First version almost finished

1 files changed, 14 insertions, 13 deletions

diff --git a/paper/intro-while.tex b/paper/intro-while.tex
index 30d8efd..128244a 100644
--- a/paper/intro-while.tex
+++ b/paper/intro-while.tex
@@ -23,26 +23,25 @@ The syntax we will use is:
 
 	<BExpr> ::= `true'
 		| `false'
-		| $a_1 = a_2$
+		\alt $a_1 = a_2$
 		| $a_1 \le a_2$
 		| $\lnot b$
 		| $b_1 \land b_2$
 
 	<Stm> ::=
 		  $x$ `:=' $a$
-		| $S_1$ `;' $S_2$
 		| `skip'
-		| `if' $b$ `then' $S_1$ `else' $S_2$ `endif'
-		| `while' $b$ `do' $S$ `done'
+		| `while' $b$ `do' $S$
+		\alt `if' $b$ `then' $S_1$ `else' $S_2$
+		| $S_1$ `;' $S_2$
 \end{grammar}
 
-The syntax of statements has been adapted slightly to make it deterministic.
-The grammar for \<Aexpr> and \<BExpr> has not been made deterministic for
-brevity's sake; standard operator precedence applies.
-
-We assume that composition (\whcomp{$S_1$}{$S_2$}) is right associative. We
-ignore all whitespace, and do not allow variable names that are reserved
-keywords such as \whskip.
+Since we do not discuss parsing in this paper, we need not modify the syntax to
+make it deterministic. Standard operator precedence applies for \<AExpr> and
+\<BExpr>; for \`while' and \`if' we let it be clear from the context where the
+block ends. Lastly, we assume that composition (\whcomp{$S_1$}{$S_2$}) is right
+associative. We ignore all whitespace, and do not allow variable names that are
+reserved keywords such as \whskip.
 
 The semantics of these syntax constructs should be intuitive. As an example,
 after executing the following program, \verb$y$ will have been divided by $2$:
@@ -52,8 +51,10 @@ after executing the following program, \verb$y$ will have been divided by $2$:
 		{\whass{x}{y}}
 		{\whwhile{\whnotp{\whle{x}{0}}}%
 			{\whcomp%
-				{x := x - 2}%
-				{y := y - 1}%
+				{\whass{x}{x-2}}
+				{\whass{y}{y-1}}
 			}
 		}
 \end{while}
+
+While programs are executed in a \emph{state} which maps variables to integers.