diff options
Diffstat (limited to 'proof.tex')
| -rw-r--r-- | proof.tex | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -159,7 +159,7 @@ A similar specification is created for the load. We then also prove that the im \subsubsection{From Specification to Simulation} -Another simulation proof is performed to prove that the insertion of the RAM is semantics preserving. As in the simulation proof shown in Lemma~\ref{lemma:simulation_diagram}, some invariants need to be defined, which always hold at the start of the simulation and at the end of the simulation. The invariants needed for the simulation of the RAM insertion are quite different to the previous invariants, so we can define these invariants $\mathcal{I}_{r}$ to be the following: +Another simulation proof is performed to prove that the insertion of the RAM is semantics preserving. As in Lemma~\ref{lemma:simulation_diagram}, we require some invariants that always hold at the start and end of the simulation. The invariants needed for the simulation of the RAM insertion are quite different to the previous ones, so we can define these invariants $\mathcal{I}_{r}$ to be the following: \begin{itemize} \item The association map for arrays $\Gamma_{a}$ always needs to have the same arrays present, and these arrays should never change in size. |