Changeset 1724 for Deliverables/D1.2/CompilerProofOutline

Timestamp:

Feb 23, 2012, 12:51:04 PM (9 years ago)

Author:

boender

Message:

• added diagrams to RTL to ERTL section

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (1 diff)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -158 +158 @@
 \begin{displaymath}
 \begin{diagram}
-        &                         & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket &                         & \\
-        & \ldTo^{\text{external}} &                                                                                               & \rdTo^{\text{internal}} & \\
- \skull &                         &                                                                                               &                         & FINISH ME
-\end{diagram}
-\end{displaymath}
+& & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket & & \\
+& \ldTo^{\text{external}} & & \rdTo^{\text{internal}} & \\
+\skull & & & & \mathtt{regs} = [\mathtt{params}/-] \\
+& & & & \mathtt{sp} = \mathtt{ALLOC} \\
+& & & & \mathtt{PUSH}(\mathtt{carry}, \mathtt{regs}, \mathtt{dst}, \mathtt{return\_addr}), \mathtt{pc}_{0}, \mathtt{regs}, \mathtt{sp} \\
+\end{diagram}
+\end{displaymath}
+
+\begin{align*}
+\llbracket \mathtt{RETURN} \rrbracket \\
+\mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\
+v*                    & := m(\mathtt{rv\_regs}) \\
+\mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\
+\mathtt{regs}[v* / \mathtt{dst}] \\
+\end{align*}
+
+\begin{displaymath}
+\begin{diagram}
+s    & \rTo^1 & s' & \rTo^1 & s'' \\
+\dTo &        &    & \rdTo  & \dTo \\
+\llbracket s \rrbracket & \rTo(1,3)^1 & & & \llbracket s'' \rrbracket \\ 
+\mathtt{CALL} \\
+\end{diagram}
+\end{displaymath}
+
+\begin{displaymath}
+\begin{diagram}
+s    & \rTo^1 & s' & \rTo^1 & s'' \\
+\dTo &        &    & \rdTo  & \dTo \\
+\  & \rTo(1,3) & & & \ \\
+\mathtt{RETURN} \\
+\end{diagram}
+\end{displaymath}
+
+\begin{displaymath}
+\mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist'})
+\rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
+\end{displaymath}
+
+\begin{align*}
+\mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\
+& \forall  f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\
+&       \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (\mathtt{next}\ l\ G_{i})\ G_{\sigma}
+\end{align*}
+
+\begin{align*}
+\mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\
+&       \forall s.  \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\
+&       \mathtt{let}\ l := pc\ s\ \mathtt{in} \\
+&       s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma
+\end{align*}
 
 \section{The ERTL to LTL translation}