Changeset 1779 for Deliverables/D1.2/CompilerProofOutline
- Timestamp:
- Feb 27, 2012, 5:11:57 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/CompilerProofOutline/outline.tex
r1778 r1779 734 734 \end{align*} 735 735 736 Translation and execution must satisfy a pair of commutation properties for the \texttt{Return} and \texttt{Call} cases. 737 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. 738 This is exemplified by the following diagram: 736 739 \begin{displaymath} 737 740 \begin{diagram} … … 739 742 \dTo & & & \rdTo & \dTo \\ 740 743 \llbracket s \rrbracket & \rTo(1,3)^1 & & & \llbracket s'' \rrbracket \\ 741 \mathtt{CALL} \\742 \end{diagram}743 \end{displaymath}744 745 \begin{displaymath}746 \begin{diagram}747 s & \rTo^1 & s' & \rTo^1 & s'' \\748 \dTo & & & \rdTo & \dTo \\749 \ & \rTo(1,3) & & & \ \\750 \mathtt{RETURN} \\751 744 \end{diagram} 752 745 \end{displaymath}
Note: See TracChangeset
for help on using the changeset viewer.