diff options
Diffstat (limited to 'papers/cfrontend_new/dynsem4.etex')
-rwxr-xr-x | papers/cfrontend_new/dynsem4.etex | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/papers/cfrontend_new/dynsem4.etex b/papers/cfrontend_new/dynsem4.etex new file mode 100755 index 00000000..3f0b10af --- /dev/null +++ b/papers/cfrontend_new/dynsem4.etex @@ -0,0 +1,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} |