Ignore:
Timestamp:
Jun 17, 2013, 12:11:13 PM (6 years ago)
Author:
sacerdot
Message:

15 pages version

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-policy/proof.tex

    r3353 r3361  
    22
    33In this section, we present the correctness proof for the algorithm in more
    4 detail.  The main correctness statement is as follows (slightly simplified, here):
    5 
     4detail.  The main correctness statement is shown, slightly simplified, in~Figure~\cite{statement}.
     5
     6\begin{figure}[t]
    67\begin{alignat*}{6}
    78\mathtt{sigma}&\omit\rlap{$\mathtt{\_policy\_specification} \equiv
     
    2021        &&&&& pc + (\mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}))
    2122\end{alignat*}
     23\caption{Main correctness statement\label{statement}}
     24\end{figure}
    2225
    2326Informally, this means that when fetching a pseudo-instruction at $ppc$, the
Note: See TracChangeset for help on using the changeset viewer.