summaryrefslogtreecommitdiff
path: root/paper/intro-while.tex
diff options
context:
space:
mode:
authorCamil Staps2016-06-03 00:39:37 +0200
committerCamil Staps2016-06-03 00:39:37 +0200
commit6ecadcb8571712536f9d121264f67f30f7bb0147 (patch)
tree0542e10ca752f538195095713ca786ab494335b6 /paper/intro-while.tex
parentUpdate example program (diff)
First version almost finished
Diffstat (limited to 'paper/intro-while.tex')
-rw-r--r--paper/intro-while.tex27
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.