Changeset 1717 for Deliverables/D1.2/CompilerProofOutline
- Timestamp:
- Feb 22, 2012, 11:28:49 AM (9 years ago)
- Location:
- Deliverables/D1.2/CompilerProofOutline
- Files:
-
- 1 added
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/CompilerProofOutline/outline.tex
r1716 r1717 6 6 \usepackage{amssymb} 7 7 \usepackage[english]{babel} 8 \usepackage{diagrams} 8 9 \usepackage[colorlinks]{hyperref} 9 10 \usepackage{microtype} … … 85 86 \end{displaymath} 86 87 88 \begin{displaymath} 89 \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})) 90 \end{displaymath} 91 92 \begin{displaymath} 93 \sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step} 94 \end{displaymath} 95 96 \begin{displaymath} 97 \sigma(\mathtt{State}(-)) \longrightarrow \sigma \circ \text{state one step} 98 \end{displaymath} 99 100 \begin{diagram} 101 \end{diagram} 102 87 103 \section{The RTL to ERTL translation} 88 104 \label{sect.rtl.ertl.translation}
Note: See TracChangeset
for help on using the changeset viewer.