Changeset 2084


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

Legend:

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

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

    r2064 r2084  
    44\usepackage{amsfonts}
    55\usepackage[british]{babel}
     6\usepackage{hyperref}
    67\usepackage[utf8]{inputenc}
    78\usepackage{listings}
     
    1415
    1516\mainmatter
    16 \title{On the correctness of a branch displacement algorithm}
     17\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}}
    1718\author{Jaap Boender \and Claudio Sacerdoti Coen}
    18 \institute{Alma Mater Studiorum---Università degli Studi di Bologna}
     19\institute{Dipartimento di Scienze dell'Informazione, Università degli Studi di Bologna}
    1920
    2021\maketitle
     
    4142
    4243\bibliography{biblio}
    43 \bibliographystyle{plain}
     44\bibliographystyle{splncs03}
    4445
    4546\end{document}
  • src/ASM/CPP2012-policy/proof.tex

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