Changeset 1717 for Deliverables/D1.2/CompilerProofOutline

Timestamp:

Feb 22, 2012, 11:28:49 AM (9 years ago)

Author:

mulligan

Message:

added diagrams.sty for drawing commutative diagrams

Location:

Deliverables/D1.2/CompilerProofOutline

Files:

• diagrams.sty (added)
• outline.tex (modified) (2 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -6 +6 @@
 \usepackage{amssymb}
 \usepackage[english]{babel}
+\usepackage{diagrams}
 \usepackage[colorlinks]{hyperref}
 \usepackage{microtype}
@@ -85 +86 @@
 \end{displaymath}
 
+\begin{displaymath}
+\sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{Frame})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), 0, 0, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem}))
+\end{displaymath}
+
+\begin{displaymath}
+\sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step}
+\end{displaymath}
+
+\begin{displaymath}
+\sigma(\mathtt{State}(-)) \longrightarrow \sigma \circ \text{state one step}
+\end{displaymath}
+
+\begin{diagram}
+\end{diagram}
+
 \section{The RTL to ERTL translation}
 \label{sect.rtl.ertl.translation}