Ignore:
Timestamp:
Feb 22, 2012, 1:54:08 PM (8 years ago)
Author:
mulligan
Message:

added skull.sty for daemon (skull) symbol

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1717 r1718  
    99\usepackage[colorlinks]{hyperref}
    1010\usepackage{microtype}
     11\usepackage{skull}
     12\usepackage{stmaryrd}
    1113
    1214\title{Proof outline for the correctness of the CerCo compiler}
     
    9597
    9698\begin{displaymath}
    97 \sigma(\mathtt{State}(-)) \longrightarrow \sigma \circ \text{state one step}
     99\sigma(\mathtt{Call}(-)) \longrightarrow \sigma \circ \text{call one step}
    98100\end{displaymath}
    99101
     102Return one step commuting diagram:
     103
     104\begin{displaymath}
    100105\begin{diagram}
     106s & \rTo^{\text{one step of execution}} & s'   \\
     107  & \rdTo                             & \dTo \\
     108  &                                   & \llbracket s'' \rrbracket
    101109\end{diagram}
     110\end{displaymath}
     111
     112Call one step commuting diagram:
     113
     114\begin{displaymath}
     115\begin{diagram}
     116s & \rTo^{\text{one step of execution}} & s'   \\
     117  & \rdTo                             & \dTo \\
     118  &                                   & \llbracket s'' \rrbracket
     119\end{diagram}
     120\end{displaymath}
     121
     122\begin{displaymath}
     123\begin{diagram}
     124\mathtt{CALL}(\mathtt{id},\ \mathtt{args},\ \mathtt{dst},\ \mathtt{pc}),\ \mathtt{State}(\mathtt{Frame},\ \mathtt{Frames}) & \rTo & \mathtt{Call}(FINISH ME)
     125\end{diagram}
     126\end{displaymath}
     127
     128\begin{displaymath}
     129\begin{array}{rcl}
     130\mathtt{CALL}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc}) & \longrightarrow & \mathtt{CALL\_ID}(\mathtt{id}, \sigma'(\mathtt{args}), \sigma(\mathtt{dst}), \mathtt{pc}) \\
     131\mathtt{RETURN}                                                      & \longrightarrow & \mathtt{RETURN} \\
     132\end{array}
     133\end{displaymath}
     134
     135\begin{displaymath}
     136\begin{array}{rcl}
     137\sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\
     138\sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register}
     139\end{array}
     140\end{displaymath}
     141
     142\begin{displaymath}
     143\begin{diagram}
     144        &                         & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket &                         & \\
     145        & \ldTo^{\text{external}} &                                                                                               & \rdTo^{\text{internal}} & \\
     146 \skull &                         &                                                                                               &
     147\end{diagram}
     148\end{displaymath}
    102149
    103150\section{The RTL to ERTL translation}
Note: See TracChangeset for help on using the changeset viewer.