Changeset 1724 for Deliverables


Ignore:
Timestamp:
Feb 23, 2012, 12:51:04 PM (8 years ago)
Author:
boender
Message:
  • added diagrams to RTL to ERTL section
File:
1 edited

Legend:

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

    r1723 r1724  
    158158\begin{displaymath}
    159159\begin{diagram}
    160         &                         & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket &                         & \\
    161         & \ldTo^{\text{external}} &                                                                                               & \rdTo^{\text{internal}} & \\
    162  \skull &                         &                                                                                               &                         & FINISH ME
    163 \end{diagram}
    164 \end{displaymath}
     160& & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket & & \\
     161& \ldTo^{\text{external}} & & \rdTo^{\text{internal}} & \\
     162\skull & & & & \mathtt{regs} = [\mathtt{params}/-] \\
     163& & & & \mathtt{sp} = \mathtt{ALLOC} \\
     164& & & & \mathtt{PUSH}(\mathtt{carry}, \mathtt{regs}, \mathtt{dst}, \mathtt{return\_addr}), \mathtt{pc}_{0}, \mathtt{regs}, \mathtt{sp} \\
     165\end{diagram}
     166\end{displaymath}
     167
     168\begin{align*}
     169\llbracket \mathtt{RETURN} \rrbracket \\
     170\mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\
     171v*                    & := m(\mathtt{rv\_regs}) \\
     172\mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\
     173\mathtt{regs}[v* / \mathtt{dst}] \\
     174\end{align*}
     175
     176\begin{displaymath}
     177\begin{diagram}
     178s    & \rTo^1 & s' & \rTo^1 & s'' \\
     179\dTo &        &    & \rdTo  & \dTo \\
     180\llbracket s \rrbracket & \rTo(1,3)^1 & & & \llbracket s'' \rrbracket \\
     181\mathtt{CALL} \\
     182\end{diagram}
     183\end{displaymath}
     184
     185\begin{displaymath}
     186\begin{diagram}
     187s    & \rTo^1 & s' & \rTo^1 & s'' \\
     188\dTo &        &    & \rdTo  & \dTo \\
     189\  & \rTo(1,3) & & & \ \\
     190\mathtt{RETURN} \\
     191\end{diagram}
     192\end{displaymath}
     193
     194\begin{displaymath}
     195\mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist'})
     196\rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
     197\end{displaymath}
     198
     199\begin{align*}
     200\mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\
     201& \forall  f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\
     202&       \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (\mathtt{next}\ l\ G_{i})\ G_{\sigma}
     203\end{align*}
     204
     205\begin{align*}
     206\mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\
     207&       \forall s.  \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\
     208&       \mathtt{let}\ l := pc\ s\ \mathtt{in} \\
     209&       s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma
     210\end{align*}
    165211
    166212\section{The ERTL to LTL translation}
Note: See TracChangeset for help on using the changeset viewer.