# Changeset 1793 for Deliverables/D1.2

Ignore:
Timestamp:
Feb 28, 2012, 5:57:46 PM (9 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r1792 \begin{displaymath} \begin{diagram} s & \rTo^{\text{one step of execution}} & s'   \\ s & \rTo^1 & s'   \\ & \rdTo                             & \dTo \\ &                                   & \llbracket s'' \rrbracket \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} 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} \end{diagram} \end{displaymath} Two steps of execution are simulated by a single step. \subsection{The RTL to ERTL translation}