\relax 
\citation{bib:mondexwww}
\citation{bib:mondexwwwcom}
\citation{bib:z}
\citation{bib:zref}
\citation{bib:specif}
\select@language{english}
\@writefile{toc}{\select@language{english}}
\@writefile{lof}{\select@language{english}}
\@writefile{lot}{\select@language{english}}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}The \emph  {Mondex} case study}{1}}
\citation{bib:alloy}
\citation{bib:alloybook}
\citation{bib:aa}
\citation{bib:kodkod}
\citation{bib:kodkodwww}
\citation{bib:trans}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2}The Alloy model-finding method}{2}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces \emph  {Concrete 5-step protocol, with the statuses of the purses depending on the operations.}}}{2}}
\newlabel{fig:proto}{{1}{2}}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces The \emph  {Alloy} model-finding method}}{3}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces The \emph  {Alloy} syntax (simplified)}}{3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3}Overview of the main issues encountered while writing the Alloy specification}{3}}
\citation{bib:mondextech}
\citation{bib:mondextechwww}
\@writefile{toc}{\contentsline {section}{\numberline {2}Representing integers with Alloy}{4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Using an order rather than sequence numbers}{4}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}Representing amounts through coins}{4}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.2.1}Computing with coins}{4}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.2.2}Defining constraints to avoid coin sharing}{5}}
\newlabel{1@xvr}{{}{5}}
\newlabel{1@vr}{{}{5}}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces {\relax \fontsize  {8}{9.5}\selectfont  \abovedisplayskip 6\p@ plus2\p@ minus4\p@ \abovedisplayshortskip \z@ plus\p@ \belowdisplayshortskip 3\p@ plus\p@ minus2\p@ \def \leftmargin \leftmargini \topsep 3\p@ plus\p@ minus\p@ \parsep 2\p@ plus\p@ minus\p@ \itemsep \parsep {\leftmargin \leftmargini \topsep 3\p@ plus\p@ minus\p@ \parsep 2\p@ plus\p@ minus\p@ \itemsep \parsep }\belowdisplayskip \abovedisplayskip Alloy definitions of the }\emph  {\relax \fontsize  {8}{9.5}\selectfont  \abovedisplayskip 6\p@ plus2\p@ minus4\p@ \abovedisplayshortskip \z@ plus\p@ \belowdisplayshortskip 3\p@ plus\p@ minus2\p@ \def \leftmargin \leftmargini \topsep 3\p@ plus\p@ minus\p@ \parsep 2\p@ plus\p@ minus\p@ \itemsep \parsep {\leftmargin \leftmargini \topsep 3\p@ plus\p@ minus\p@ \parsep 2\p@ plus\p@ minus\p@ \itemsep \parsep }\belowdisplayskip \abovedisplayskip definitelyLost}{\relax \fontsize  {8}{9.5}\selectfont  \abovedisplayskip 6\p@ plus2\p@ minus4\p@ \abovedisplayshortskip \z@ plus\p@ \belowdisplayshortskip 3\p@ plus\p@ minus2\p@ \def \leftmargin \leftmargini \topsep 3\p@ plus\p@ minus\p@ \parsep 2\p@ plus\p@ minus\p@ \itemsep \parsep {\leftmargin \leftmargini \topsep 3\p@ plus\p@ minus\p@ \parsep 2\p@ plus\p@ minus\p@ \itemsep \parsep }\belowdisplayskip \abovedisplayskip {} and }\emph  {\relax \fontsize  {8}{9.5}\selectfont  \abovedisplayskip 6\p@ plus2\p@ minus4\p@ \abovedisplayshortskip \z@ plus\p@ \belowdisplayshortskip 3\p@ plus\p@ minus2\p@ \def \leftmargin \leftmargini \topsep 3\p@ plus\p@ minus\p@ \parsep 2\p@ plus\p@ minus\p@ \itemsep \parsep {\leftmargin \leftmargini \topsep 3\p@ plus\p@ minus\p@ \parsep 2\p@ plus\p@ minus\p@ \itemsep \parsep }\belowdisplayskip \abovedisplayskip maybeLost}{\relax \fontsize  {8}{9.5}\selectfont  \abovedisplayskip 6\p@ plus2\p@ minus4\p@ \abovedisplayshortskip \z@ plus\p@ \belowdisplayshortskip 3\p@ plus\p@ minus2\p@ \def \leftmargin \leftmargini \topsep 3\p@ plus\p@ minus\p@ \parsep 2\p@ plus\p@ minus\p@ \itemsep \parsep {\leftmargin \leftmargini \topsep 3\p@ plus\p@ minus\p@ \parsep 2\p@ plus\p@ minus\p@ \itemsep \parsep }\belowdisplayskip \abovedisplayskip {} sets of transactions}}}{6}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {2.2.3}Redefining \emph  {chosenLost} set : coins as a tracking system}{6}}
\citation{bib:ooz}
\@writefile{toc}{\contentsline {section}{\numberline {3}Records in Z, objects in Alloy}{7}}
\newlabel{sub:ident}{{3.1}{7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}The identity of objects}{7}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.1.1}Simulating objects with Z records and names}{7}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.1.2}Simulating records with Alloy objects : canonicalization}{7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Consequence : existential quantification and constraints}{7}}
\citation{bib:specif}
\@writefile{toc}{\contentsline {section}{\numberline {4}Results}{9}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Bugs found in the Z specification}{9}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {4.1.1}Abort proof schema}{9}}
\citation{bib:eves}
\citation{bib:kiv}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {4.1.2}Framing schema for operations that first abort}{10}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {4.1.3}Authenticity}{10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Scopes and times of checks}{10}}
\citation{bib:frias}
\citation{bib:smt}
\citation{bib:prioni}
\citation{bib:athena}
\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces \emph  {Time exponentially increases with the scope}}}{11}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Limits to the use of the \emph  {Alloy Analyzer}}{11}}
\citation{bib:frias}
\citation{bib:smt}
\citation{bib:prioni}
\citation{bib:mondextech}
\citation{bib:tptp}
\citation{bib:tcfol}
\citation{bib:frias}
\bibstyle{alpha}
\bibdata{mondex-alloy}
\bibcite{bib:aa}{AA}
\bibcite{bib:prioni}{AKMR03}
\bibcite{bib:athena}{Ath}
\bibcite{bib:frias}{FPB{$^{+}$}05}
\bibcite{bib:eves}{FW06}
\bibcite{bib:ooz}{Hal90}
\bibcite{bib:trans}{Jac00}
\bibcite{bib:alloy}{Jac02}
\bibcite{bib:alloybook}{Jac06}
\bibcite{bib:tcfol}{LAIR{$^{+}$}05}
\bibcite{bib:mondexwww}{MCS}
\bibcite{bib:smt}{Mom04}
\bibcite{bib:mondexwwwcom}{Mon}
\bibcite{bib:mondextechwww}{Ram}
\bibcite{bib:mondextech}{Ram06}
\bibcite{bib:specif}{SCW00}
\bibcite{bib:kiv}{SGHR06}
\@writefile{toc}{\contentsline {section}{\numberline {5}Conclusion and related work}{12}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Acknowledgments}{12}}
\@writefile{toc}{\contentsline {section}{References}{12}}
\bibcite{bib:z}{Spi92}
\bibcite{bib:kodkod}{TJ07}
\bibcite{bib:kodkodwww}{Tor}
\bibcite{bib:tptp}{TPT}
\bibcite{bib:zref}{WD96}