Changeset 1779 for Deliverables/D1.2/CompilerProofOutline

Timestamp:

Feb 27, 2012, 5:11:57 PM (8 years ago)

Author:

mulligan

Message:

...

File:

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

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -734 +734 @@
 \end{align*}
 
+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:
 \begin{displaymath}
 \begin{diagram}
@@ -739 +742 @@
 \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}