blob: bdf2858c963692c9840c51303bf28aea7f9a5e42 (
plain)
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
|
\begin{figure}
\begin{syntax}
\syntaxclass{Values:}
\loc & ::= & (b, n) & location (byte offset $n$ in the memory block\\
& & & referenced by $b$)\\
v & ::= & n & integer value\\
& \alt & f & floating-point value \\
& \alt & \loc & pointer value\\
% v & ::= & "Vint"(n) & integer value\\
% & \alt & "Vfloat"(f) & floating-point value \\
% & \alt & "Vptr"(\loc) & pointer value\\
& \alt & "Vundef" & undefined value
%
\syntaxclass{Statement outcomes:}
\out & ::= & "Out_normal" & go to the next statement \\
& \alt & "Out_continue" & go to the next iteration of the current loop \\
& \alt & "Out_break" & exit from the current loop \\
& \alt & "Out_return" & function exit \\
& \alt & "Out_return"(v) & function exit, returning the value $v$
%
\syntaxclass{Global environments:}
G & ::= & (id \mapsto b) & map from global variables to block references \\
& & \times (b \mapsto \fn) & and map from function references \\
& & & to function definitions
%
\syntaxclass{Local environments:}
E & ::= & \id \mapsto b & map from local variables to block references
%
\syntaxclass{Memories:}
{\it bounds} & ::= & \ldots & low and high bounds \\
{\it kind} & ::= & \ldots & content map \\
M & ::= & b \mapsto {\it bounds} \times & map from block references to block contents\\
& & (n \mapsto {\it kind} \mapsto v) &
\end{syntax}
%
\caption{Values, outcomes, and evaluation environments}
\label{fig:values}
\end{figure}
|
