Ignore:
Timestamp:
Jun 15, 2012, 5:29:10 PM (7 years ago)
Author:
boender
Message:
  • updates & changes
File:
1 edited

Legend:

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

    r2096 r2098  
    33In this section, we present the correctness proof for the algorithm in more
    44detail.  The main correctness statement is as follows (slightly simplified, here):
    5 
    6 \clearpage
    75
    86\begin{lstlisting}
     
    114112
    115113\clearpage
    116 
    117114\begin{lstlisting}
    118115definition sigma_compact_unsafe :=
     
    200197We need to use two different formulations, because the fact that $added$ is 0
    201198does not guarantee that no branch instructions have changed.  For instance,
    202 it is possible that we have replaced a short jump with a absolute jump, which
     199it is possible that we have replaced a short jump with an absolute jump, which
    203200does not change the size of the branch instruction.
    204201
     
    224221If an iteration returns {\tt None}, we have the following invariant:
    225222
     223\clearpage
    226224\begin{lstlisting}
    227225definition nec_plus_ultra :=
Note: See TracChangeset for help on using the changeset viewer.