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 0000000..3f0b10a
--- /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}