# Changeset 2084

Ignore:
Timestamp:
Jun 15, 2012, 1:17:15 AM (7 years ago)
Message:
• changed bibliography style
• added CerCo? thanks
• some words of conclusion
Location:
src/ASM/CPP2012-policy
Files:
1 added
3 edited

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

 r2064 \section{Conclusion} In the previous sections, we have discussed the branch displacement optimisation problem, presented an optimised solution, and discussed the proof of termination and correctness for this algorithm, as formalised in Matita. \subsection{Related work} As far as we are aware, this is the first formal discussion of the branch displacement algorithm. (Piton? CompCert?) \subsection{Formal development} All Matita files related to this development can be found on the CerCo website, \url{http://cerco.cs.unibo.it}. The specific part that contains the branch displacement algorithm is in the {\tt ASM} subdirectory, in the files whose name starts with {\tt Policy}.
• ## src/ASM/CPP2012-policy/main.tex

 r2064 \usepackage{amsfonts} \usepackage[british]{babel} \usepackage{hyperref} \usepackage[utf8]{inputenc} \usepackage{listings} \mainmatter \title{On the correctness of a branch displacement algorithm} \title{On the correctness of a branch displacement algorithm\thanks{Research supported by the CerCo project, within the Future and Emerging Technologies (FET) programme of the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number 243881}} \author{Jaap Boender \and Claudio Sacerdoti Coen} \institute{Alma Mater Studiorum---Università degli Studi di Bologna} \institute{Dipartimento di Scienze dell'Informazione, Università degli Studi di Bologna} \maketitle \bibliography{biblio} \bibliographystyle{plain} \bibliographystyle{splncs03} \end{document}
• ## src/ASM/CPP2012-policy/proof.tex

 r2082 program size. Here, we only need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that $\sigma(0) = 0$. Termination can now be proven through the fact that there is a $k \leq 2n$, with $n$ the length of the program, such that iteration $k$ is equal to iteration $k+1$. There are two possibilities: either there is a $k < 2n$ such that this property holds, or every iteration up to $2n$ is different. In the latter case, since the only changes between the iterations can be from shorter jumps to longer jumps, in iteration $2n$ every jump must be long. In this case, iteration $2n$ is equal to iteration $2n+1$ and the fixpoint is reached.
Note: See TracChangeset for help on using the changeset viewer.