blob: 128244a2faef39839893d3ba615d46375737fff0 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
\subsection{The language While}
\label{sec:intro:while}
We will use the language While described by~\cite{proganal} as a running
example. In its definition, we use the following meta-variables:
\begin{tabbing}
\qquad \= $n$ \enspace\= denotes an integer; \\
\> $x$ \> a variable name; \\
\> $a$ \> an arithmetical expression (\synt{AExpr}); \\
\> $b$ \> a boolean expression (\synt{BExpr}); and \\
\> $S$ \> a statement (\synt{Stm}).
\end{tabbing}
The syntax we will use is:
\grammarindent=6em
\begin{grammar}
<AExpr> ::= $n$
| $x$
| $a_1 + a_2$
| $a_1 \times a_2$
| $a_1 - a_2$
<BExpr> ::= `true'
| `false'
\alt $a_1 = a_2$
| $a_1 \le a_2$
| $\lnot b$
| $b_1 \land b_2$
<Stm> ::=
$x$ `:=' $a$
| `skip'
| `while' $b$ `do' $S$
\alt `if' $b$ `then' $S_1$ `else' $S_2$
| $S_1$ `;' $S_2$
\end{grammar}
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$:
\begin{while}
\whcomp%
{\whass{x}{y}}
{\whwhile{\whnotp{\whle{x}{0}}}%
{\whcomp%
{\whass{x}{x-2}}
{\whass{y}{y-1}}
}
}
\end{while}
While programs are executed in a \emph{state} which maps variables to integers.
|
