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
|
\begin{figure}
\numberrules
Execution of a "switch" statement:
\begin{pannel}
\irule
G, E |- a, M \evalexpr n, \tr, M_1 \\
G, E |- "select_switch" (n,\ls), M_1 \evalstmt \out, \tr_2, M_2
--------------------------------------------------
G, E |- "switch" (a)\ls, M \evalstmt "outcome_switch" (\out), \cat {\tr_1} \tr_2, M_2
\end \label{rule:28}
\end{pannel}
Execution of a "switch" branch:
\begin{pannel}
\irule
G, E |- s, M \evalstmt \out, \tr, M'
--------------------------------------------------
G, E |- "default" (s) , M \evalstmt \out, \tr, M'
\end \label{rule:29}
\\
\irule
G, E |- s, M \evalstmt "Out_normal", \tr_1, M_1 \\
G, E |- \ls, M \evalstmt \out, \tr_2, M_2
--------------------------------------------------
G, E |- "case" (n,s,\ls), M \evalstmt \out', \tr_2, M_2
\end \label{rule:30}
\\
\irule
G, E |- s, M \evalstmt \out, \tr, M' & \out \not= "Out_normal"
--------------------------------------------------
G, E |- "case" (n,s,\ls), M \evalstmt \out', \tr, M'
\end \label{rule:31}
\end{pannel}
\caption{Dynamic semantics of switch statement}
\label{fig:dynsem4}
\end{figure}
|
