# Changeset 2098 for src/ASM/CPP2012-policy/proof.tex

Ignore:
Timestamp:
Jun 15, 2012, 5:29:10 PM (8 years ago)
Message:
 r2096 In this section, we present the correctness proof for the algorithm in more detail.  The main correctness statement is as follows (slightly simplified, here): \clearpage \begin{lstlisting} \clearpage \begin{lstlisting} definition sigma_compact_unsafe := We need to use two different formulations, because the fact that $added$ is 0 does not guarantee that no branch instructions have changed.  For instance, it is possible that we have replaced a short jump with a absolute jump, which it is possible that we have replaced a short jump with an absolute jump, which does not change the size of the branch instruction. If an iteration returns {\tt None}, we have the following invariant: \clearpage \begin{lstlisting} definition nec_plus_ultra :=