\documentclass[a4paper]{report}

\usepackage{hyperref}
\usepackage{color}
\usepackage{graphicx}
\usepackage{wrapfig}
\usepackage{alltt}
\usepackage{remreset}

% Disable resetting footnote counter at new chapter
\makeatletter\@removefromreset{footnote}{chapter}\makeatother

%% define highlight command
\newcommand{\highlight}[1]{\textcolor{blue}{\textbf{#1}}}

%% define code environment
\newenvironment{code}
{\begin{list}{}
{\setlength{\leftmargin}{1em}}\item\normalsize\bfseries}
{\end{list}}

\parindent 0pt

%--------------------------------------------------------------------

\begin{document}
\begin{titlepage}
	\null
	\vfill
	\begin{center}\leavevmode
		\normalfont
		{\Huge A Guide To Alloy\par}
		\vskip 1.5cm
		{\LARGE Second Year Group Project\par}
		\vskip 1cm
		{\large Edward Yue Shung Wong, Michael Herrmann, Omar Tayeb \\ Supervisor: Dr. Krysia Broda\par}
	\end{center}
	\vfill
	\null
\end{titlepage}

\begin{abstract}
Specification languages are a large part of Software Engineering. 
Learning how to write a rigorous model is a fundamental part of designing 
good code. This report aims to explore the Alloy specification language, 
its application through the Alloy Analyzer tool and its potential in teaching. By writing a 
\htmladdnormallink{website}{http://www.doc.ic.ac.uk/project/2007/271j/g06271j01/Web/}
\footnote{http://www.doc.ic.ac.uk/project/2007/271j/g06271j01/Web/}
aimed at conveying Alloy to our peers, we were able to experience first-hand 
the intricacies of Alloy. We found that Alloy is a highly intuitive language 
that lends itself well as an introduction to formal specification languages. 
The simplistic synthax and the well developed Alloy Analyzer tool makes 
Alloy highly condusive to quick learning. As a result of this report we 
hope Alloy will see more widespread use in education as well as encouraging 
further development of the language itself.
\end{abstract}

%--------------------------------------------------------------------
\renewcommand\thepage{}
\tableofcontents
\setcounter{page}{0}
\newpage
\renewcommand\thepage{\arabic{page}}
%--------------------------------------------------------------------

% Edward's section
\include{A_Guide_To_Alloy}

%--------------------------------------------------------------------

% Michael's section
\include{Koenigsberg}

%--------------------------------------------------------------------
% Omar's section
\include{web_design}

%--------------------------------------------------------------------

% Michael's section
\include{Conclusion_Evaluation}

%--------------------------------------------------------------------

% Omar's section
\pagestyle{empty}
\include{glossary}
\include{files}

%--------------------------------------------------------------------
\begin{thebibliography}{9}
\addcontentsline{toc}{chapter}{Bibliography}
	\bibitem{mitFAQ} Alloy MIT website, FAQ section: http://alloy.mit.edu/faq.php
	\bibitem{jackson06} Jackson, D. \emph{Software Abstractions: Logic, Language and Analysis}, MIT Press, 2006. 
	\bibitem{russo} Russo, A. \emph{Lecture Slides of Undergraduate Course Software Engineering I taught at Imperial College London 2007}, \htmladdnormallink{http://www.doc.ic.ac.uk/~ar3/lectures/Sed/NewCourseStructure.html}{http://www.doc.ic.ac.uk/~ar3/lectures/Sed/NewCourseStructure.html}
	\bibitem{tutorial} Alloy MIT Online Tutorial http://alloy.mit.edu/tutorial3/maintext-FS-I.html
	\bibitem{sautoy04} Du Sautoy, M. \emph{The Music of the Primes: Why an Unsolved Problem in Mathematics Matters}, Harper Perennial, 2004. 
	\bibitem{agnarsson06} Agnarsson, G., Greenlaw, R. \emph{Graph Theory: Modeling, Applications, and Algorithms}, Pearson Education, 2006. 
	\bibitem{specBox89} Froome, P. K. D., Monahan, B.Q. \& Bloomfield, R. E., \emph{Specbox - a checker for VDM specifications}, In \emph{Proc. Second Int. Conf. on Software Engineering for Real Time Systems}, 1989.
\end{thebibliography}

%--------------------------------------------------------------------

\end{document}
