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

Ignore:
Timestamp:
Jun 15, 2012, 5:56:30 PM (8 years ago)
Message:
• added reference to Intel dev manual
File:
1 edited

### Legend:

Unmodified
 r2098 \end{lstlisting} This is a temporary formulation of the main property This is a temporary formulation of the main property\\ ({\tt sigma\_policy\_specification}); its main difference from the final version is that it uses {\tt instruction\_size\_jmplen} to If the iteration returns $\mathtt{Some}\ \sigma$, the invariants {\tt out\_of\_program\_none}, {\tt not\_jump\_default}, {\tt jump\_increase}, {\tt out\_of\_program\_none},\\ {\tt not\_jump\_default}, {\tt jump\_increase}, and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are retained without change.