Changeset 1793 for Deliverables/D1.2
- Timestamp:
- Feb 28, 2012, 5:57:46 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/CompilerProofOutline/outline.tex
r1792 r1793 577 577 \begin{displaymath} 578 578 \begin{diagram} 579 s & \rTo^ {\text{one step of execution}}& s' \\579 s & \rTo^1 & s' \\ 580 580 & \rdTo & \dTo \\ 581 581 & & \llbracket s'' \rrbracket … … 583 583 \end{displaymath} 584 584 585 \begin{displaymath} 586 \begin{diagram} 587 s & \rTo^{\text{one step of execution}} & s' \\ 588 & \rdTo & \dTo \\ 589 & & \llbracket s'' \rrbracket 590 \end{diagram} 591 \end{displaymath} 592 \caption{The one-step commuting diagrams for \texttt{Call} and \texttt{Return} state translations} 585 \caption{The one-step commuting diagrams for \texttt{Call} and \texttt{Return} state translations.} 593 586 \label{fig.commuting.diagrams} 594 587 \end{figure} … … 719 712 720 713 To summarize, the forward simulation diagrams for function call/return 721 XXX 722 723 Translation and execution must satisfy a pair of commutation properties for the \texttt{Return} and \texttt{Call} cases. 724 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. 725 This is exemplified by the following diagram: 714 have the following form where the triangle is the one given in 715 Figure~\ref{fig.commuting.diagrams}, the next instruction to be 716 executed in state $s$ is either a function call or return and the intermediate 717 state $s'$ is either a \texttt{Call} or a \texttt{Return} state. 726 718 \begin{displaymath} 727 719 \begin{diagram} … … 731 723 \end{diagram} 732 724 \end{displaymath} 725 Two steps of execution are simulated by a single step. 733 726 734 727 \subsection{The RTL to ERTL translation}
Note: See TracChangeset
for help on using the changeset viewer.