\chapter{A Guide To Alloy}
	\section{Introduction}
		\subsection{Philosophy}
		Software development is difficult; choosing correct abstractions 
		to base your design around is a tricky process! Quite often apparently 
		simple and robust designs can turn out to be incoherent and even 
		inconsistent when you come to implement them.\newline


		One way to avoid this problem of "wishful thinking" as well as making 
		software development more straightforward is through formal specification. 
		This method approaches software abstraction head-on using precise and unambiguous 
		notation, one such example is the declarative language Z.\newline 


		Naturally this is not fool proof either though; proving your specification 
		is correct/sound requires a substantial amount of effort. Whilst conventional 
		theorem based analysis tools have improved, their level of automation is still 
		relatively poor compared to model checkers.\newline 


		Hence, Alloy was developed in the hope of adapting a declarative language like 
		Z to bring in fully automatic analysis. To do this Alloy sacrifices the ability 
		to totally prove a system's correctness. Rather, it attempts to find counterexamples 
		within a limited scope that violate the constraints of the system. Thus by 
		combining the best of both worlds Alloy produces a rigorous model that gives the 
		user immediate feedback.

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

		\subsection{History}		
		The design was done by the Software Design Group at MIT lead by Professor Daniel Jackson. 
		In 1997 they produced the first Alloy prototype, which was then a rather limited 
		object modelling language. Over the years Alloy has developed into a full 
		structural modelling language capable of expressing complex structural 
		constraints and behaviour.\newline 

		\newpage

		\begin{wrapfigure}{l}{0.5\textwidth}
			\begin{center}
				\includegraphics{daniel_jackson.eps}
			\end{center}
			\caption{Professor Daniel Jackson}
		\end{wrapfigure}

		By employing first order logic, Alloy is able to translate specifications into 
		large Boolean expression that can be automatically analyzed by SAT solvers. 
		Thus when given a logical formula (in Alloy), the Alloy Analyzer can 
		attempt to find a model which satisfies it.\newline


		One of the great benefits this lends to Alloy is the ability 
		of incremental analysis. A programmer may explore design ideas starting 
		from a tiny model which is then scaled up, with Alloy able to 
		analyse it at every step.\newline \newline


		Alloy has gradually improved in performance and scalability and been 
		applied to many fields including scheduling, 
		cryptography and instant messaging. 

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

	\section{Tutorial}
		\subsection{Getting Started}
		This is an adapted version of our online tutorial which is available 
		\htmladdnormallink{here}{http://www.doc.ic.ac.uk/project/2007/271j/g06271j01/Web/Tutorial_Intro.php}.\newline

		
		We will be incrementally developing examples and introducing the 
		features and concepts as we go. Keywords will be 
		\highlight{highlighted} and their definitions can be found in the glossary.\newline 


		What will be included in this tutorial:
		\begin{itemize}
		
			\item A guide to Alloy's interface and visualiser
			\item Writing a model in Alloy
			\item Troubleshooting \& Tips on Alloy

		\end{itemize}

		\newpage

		A video tutorial on using the Alloy Analyzer is available on 
		the \htmladdnormallink{website}{http://www.doc.ic.ac.uk/project/2007/271j/g06271j01/Web/Alloy\%20Demo.html} 
		as well.

		\begin{figure}
			\begin{center}
				\includegraphics{Alloy_Demo.eps}
			\end{center}
			\caption{
				\htmladdnormallink{Click to launch video!}
				{http://www.doc.ic.ac.uk/project/2007/271j/g06271j01/Web/Alloy\%20Demo.html}
			}
		\end{figure}

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

		\subsection{Statics I}
		In this tutorial, we will be using Alloy to model a linked list implementation 
		of a Queue: Every queue has a root node and each node has a reference to the next 
		node in the queue.\newline	


		Each Alloy model starts with the \highlight{module} declaration:

		\begin{code}
			\begin{alltt}      
				\highlight{module} examples/tutorial/Queue
			\end{alltt}
		\end{code}


		This is similar to declaring a class Queue in the package examples.tutorial in Java. 
		Similar to Java, the file should be named 'Queue.als' and be located in the subfolder 
		examples/tutorial of the project folder.\newline


		The first step is to declare the \highlight{signature} for the queue and its nodes:

		\begin{code}
			\begin{alltt}
				\highlight{sig} Queue { root: \highlight{lone} Node }
				\highlight{sig} Node  { next: \highlight{lone} Node }
			\end{alltt}
		\end{code}

		You can think of root and next as being fields of type Node. \highlight{lone} is a 
		multiplicity keyword which indicates that each Queue has less than or equal to one root 
		(similarly for next). \newline


		A \highlight{signature} in Alloy is similar to the signature of a schema in that it defines 
		the vocabulary for the model. \newline

		
		We can already visualize what we have written so far. The common way of doing this is to write 
		a predicate and then make Alloy produce instances that satisfy this predicate. Asking Alloy to 
		find instances is similar to finding a model of a given schema. \newline


		Because we want any instance of the Queue so far, the predicate has no constraints:


		\begin{code}
			\begin{alltt}
			\highlight{pred} show() {}
			\end{alltt}
		\end{code}

		To get sample instances of the predicate we use the command run: 

		\begin{code}
			\begin{alltt}
			\highlight{run} show \highlight{for} 2
			\end{alltt}
		\end{code}

		A very important fact about Alloy is that it is only designed to search for instances 
		within a finite scope. In the above case this scope is set to at most 2 objects in each 
		signature(i.e. at most two Queues and at most two Nodes). Note that this is always an 
		upper bound; Alloy may return a smaller instance. \newline

		In order to produce and visualize an instance, we first execute the \highlight{run} 
		command by clicking on the Execute button. After the execution has finished, 
		Alloy will tell us that it has found an instance which we can visualize 
		by clicking on the Show button. \newline

		\begin{code}
			\begin{alltt}
				\highlight{module} examples/tutorial/Queue
				\highlight{sig} Queue { root: Node }
				\highlight{sig} Node { next: \highlight{lone} Node }
				\highlight{pred} show() {}
				\highlight{run} show \highlight{for} 2
			\end{alltt}
		\end{code}

		
		\begin{figure}[h]
			\begin{center}
				\includegraphics{Example_01.eps}
			\end{center}
			\caption{Queue One}
		\end{figure}


		In the above image, we see that Node1 is its own successor. 
		As this is not what we usually expect from a linked list, 
		we add a \highlight{fact} to constrain our model: 


		\begin{code}
			\begin{alltt}
				\highlight{fact} nextNotReflexive { \highlight{no} n:Node | n = n.next }
			\end{alltt}
		\end{code}


		Facts in Alloy are 'global' in that they always apply and they correspond 
		to the axioms of a schema. When Alloy is searching for instances it will 
		discard any that violate the facts of the model. The constraint above can 
		be read just like in first order logic: there is no Node n that is equal 
		to its successor. \newline


		Executing \highlight{run} show now produces the following instance: 


		\begin{code}
			\begin{alltt}
				\highlight{module} examples/tutorial/Queue
	
				\highlight{sig} Queue { root: Node }
				\highlight{sig} Node { next: \highlight{lone} Node }
				\highlight{fact} nextNotReflexive { \highlight{no} n:Node | n = n.next }
				\highlight{pred} show() {}
				\highlight{run} show \highlight{for} 2
			\end{alltt}
		\end{code}

		\begin{figure}[h]
			\begin{center}
				\includegraphics{Example_02.eps}
			\end{center}
			\caption{Queue Two}
		\end{figure}


		We no longer have a Node that is its own successor, but now 
		notice another problem of our model: There are Nodes that do 
		not belong to any Queue.

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

		\subsection{Statics II}
		To address the issue of nodes that do not belong to any queues, we add another \highlight{fact}:


		\begin{code}
			\begin{alltt}
				\begin{tabbing}
				\highlight{fact} \= allNodesBelongToSomeQueue \{ \\
					\> \highlight{all} n:Node | \highlight{some} q:Queue | n \highlight{in} q.root.*next \\
				\}
				\end{tabbing}
			\end{alltt}
		\end{code}


		\highlight{all} and \highlight{some} behave exactly like the forall and exists quantifiers in predicate logic. 
		The .* operator represents the \emph{reflexive transitive closure}: It returns the set consisting of all elements:

		\begin{code}
			\begin{alltt}
				q.root, 
				q.root.next, 
				q.root.next.next, 
				...
			\end{alltt}
		\end{code}

		



		%--------------------------------------------------------------
		\subsection{Dynamics I}


		%--------------------------------------------------------------
		\subsection{Dynamics II}

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

	\section{Alternatives to Alloy}

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

	\section{Test Yourself!}

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

	\section{Final Thoughts}