Changeset 1793 for Deliverables/D1.2

Timestamp:

Feb 28, 2012, 5:57:46 PM (8 years ago)

Author:

sacerdot

Message:

...

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (4 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -577 +577 @@
 \begin{displaymath}
 \begin{diagram}
-s & \rTo^{\text{one step of execution}} & s'   \\
+s & \rTo^1 & s'   \\
   & \rdTo                             & \dTo \\
   &                                   & \llbracket s'' \rrbracket
@@ -583 +583 @@
 \end{displaymath}
 
-\begin{displaymath}
-\begin{diagram}
-s & \rTo^{\text{one step of execution}} & s'   \\
-  & \rdTo                             & \dTo \\
-  &                                   & \llbracket s'' \rrbracket
-\end{diagram}
-\end{displaymath}
-\caption{The one-step commuting diagrams for \texttt{Call} and \texttt{Return} state translations}
+\caption{The one-step commuting diagrams for \texttt{Call} and \texttt{Return} state translations.}
 \label{fig.commuting.diagrams}
 \end{figure}
@@ -719 +712 @@
 
 To summarize, the forward simulation diagrams for function call/return
-XXX
-
-Translation and execution must satisfy a pair of commutation properties for the \texttt{Return} and \texttt{Call} cases.
-Starting from any \texttt{Return} or \texttt{Call} state, translating and then executing a single step must be the same as executing exactly two steps and then translating, with the intermediate state obtained by executing once also being translatable to the final state.
-This is exemplified by the following diagram:
+have the following form where the triangle is the one given in
+Figure~\ref{fig.commuting.diagrams}, the next instruction to be
+executed in state $s$ is either a function call or return and the intermediate
+state $s'$ is either a \texttt{Call} or a \texttt{Return} state.
 \begin{displaymath}
 \begin{diagram}
@@ -731 +723 @@
 \end{diagram}
 \end{displaymath}
+Two steps of execution are simulated by a single step.
 
 \subsection{The RTL to ERTL translation}