Changeset 1779


Ignore:
Timestamp:
Feb 27, 2012, 5:11:57 PM (7 years ago)
Author:
mulligan
Message:

...

File:
1 edited

Legend:

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

    r1778 r1779  
    734734\end{align*}
    735735
     736Translation and execution must satisfy a pair of commutation properties for the \texttt{Return} and \texttt{Call} cases.
     737Starting 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.
     738This is exemplified by the following diagram:
    736739\begin{displaymath}
    737740\begin{diagram}
     
    739742\dTo &        &    & \rdTo  & \dTo \\
    740743\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} \\
    751744\end{diagram}
    752745\end{displaymath}
Note: See TracChangeset for help on using the changeset viewer.