\pagestyle{plain}
\chapter{A Guide To Alloy}
	\section{Introduction}
	In this report we will discuss the subject of our group project, the Alloy specification language
	and its application through the Alloy Analyzer. The website we produced as a part of this project can be found\htmladdnormallink{here}{http://www.doc.ic.ac.uk/project/2007/271j/g06271j01/Web/}
	\footnote{http://www.doc.ic.ac.uk/project/2007/271j/g06271j01/Web/}. This chapter is an adapted version of it.
	


		\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 of avoiding 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. An example of this would be 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 
		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 powerful 
		modelling language capable of expressing complex structural 
		constraints and behaviour.\newline 

		\begin{wrapfigure}{l}{0.48\textwidth}
			\begin{center}
				\includegraphics[scale=0.6]{daniel_jackson.jpg}
			\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 model (in Alloy), the Alloy Analyzer can 
		attempt to find an instance 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

		Alloy has gradually improved in performance and scalability and has 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}
		\footnote{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}\footnote{http://www.doc.ic.ac.uk/project/2007/271j/g06271j01/Web/Alloy\%20Demo.html}.

		\begin{figure}
			\begin{center}
				\includegraphics[width=\textwidth]{Alloy_Demo.jpg}
			\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}
		\label{Statics_I}
		In this section, 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 \texttt{Queue} in the package \texttt{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 \texttt{root} and \texttt{next} as being fields of type \texttt{Node}. \highlight{lone} is a 
		multiplicity keyword which indicates that each \texttt{Queue} has less than or equal to one root 
		(similarly for \texttt{next}). \newline


		A \highlight{signature} in Alloy is similar to the signature of a schema in that it defines 
		the vocabulary for the model. 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 models 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 \highlight{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 \texttt{Queues} and at most two \texttt{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 \emph{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 \emph{Show} button.

		\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[scale=0.75]{Example_01.jpg}
			\end{center}
% 			\caption{}
		\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. 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 \texttt{Node n} that is equal 
		to its successor. \newline


		Executing \highlight{run} \texttt{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[scale=0.8]{Example_02.jpg}
			\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}


		If we press Execute, Alloy tells us that it found an instance. However, when we ask it to visualize the 
		instance, it tells us that every atom is hidden. In order to get the next solution, we click Next at the top. 
		Browsing through the instances, we find that one of them contains a cycle:


		\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 \}
				\begin{tabbing}
				\highlight{fact} \=allNodesBelongToSomeQueue \{ \\
					\> \highlight{all} n:Node | \highlight{some} q:Queue | n \highlight{in} q.root.\*next \\
				\} \end{tabbing}
				\highlight{pred} show() \{\}
				\highlight{run} show \highlight{for} 2
			\end{alltt}
		\end{code}

		\begin{figure}[h]
			\begin{center}
				\includegraphics[scale=0.75]{Example_04.jpg}
			\end{center}
% 			\caption{Queue Three}
		\end{figure}


		In order to fix our model we add another \highlight{fact}:


		\begin{code}
			\begin{alltt}
				\highlight{fact} nextNotCyclic { \highlight{no} n:Node | n \highlight{in} n.\^{}next }
			\end{alltt}
		\end{code}


		In contrast to the .* operator, .\^{} represents the \emph{non-reflexive transitive closure} 
		which returns the set consisting of all elements:


		\begin{code}
			\begin{alltt}
				n.next, 
				n.next.next, 
				n.next.next.next, 
				...
			\end{alltt}
		\end{code}


		(Note that this set does not include \texttt{n} itself). \newline


		Executing, visualizing and browsing through a few instances, we spot another error: 


		\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 \}
				\begin{tabbing}
				\highlight{fact} \= allNodesBelongToSomeQueue \{ \\
					\> \highlight{all} n:Node | \highlight{some} q:Queue | n \highlight{in} q.root.\*next \\
				\}\end{tabbing}\highlight{fact} nextNotCyclic \{ \highlight{no} n:Node | n \highlight{in} n.\^{}next \}

				\highlight{pred} show() \{\}
				\highlight{run} show \highlight{for} 2
			\end{alltt}
		\end{code}

		\begin{figure}[h]
			\begin{center}
				\includegraphics[scale=0.75]{Example_03.jpg}
			\end{center}
% 			\caption{Queue Four}
		\end{figure}


		The problem here is that Node belongs to two different queues. This is because 
		\texttt{allNodesBelongToSomeQueue} constrains a Node to belong to some Queue while it should actually 
		belong to exactly one. To fix this we modify the \highlight{fact}:

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

		Browsing through the instances for this version of the model, Alloy soon tells us 
		that `there are no more satisfying instances'. All the solutions found within the scope 
		provided seem to be correct. To gain more confidence, we increase the scope further:

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

		Still, we cannot find any instances that clash with our definition of a linked list and 
		conclude that this seems to be a good model for a linked list implementation of a queue. 
		However, note that this does not \emph{prove} that our model is correct! We can only guarantee 
		that it corresponds with our definition for at most three Queues and three Nodes. As Alloy 
		only ever searches a finite scope, it never allows you to prove that your model is correct. 
		However, you can gain a fair amount of confidence that the main errors have been eliminated. \newline


		Now that we have seen how to model the static aspects of a system, we will move on to 
		modelling dynamic behaviour and adding operations. For this, we will consider a different example.

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

		In this second part of the tutorial, we will be modelling a Map that associates unique keys with 
		values (such as eg. 
		\texttt{\htmladdnormallink{Map}{http://java.sun.com/j2se/1.4.2/docs/api/java/util/Map.html}}
		\footnote{http://java.sun.com/j2se/1.4.2/docs/api/java/util/Map.html}
		 in Java) and show how Alloy can be used to explore dynamic behaviour. \newline


		The static aspects are easy to specify: 

		\begin{code}
			\begin{alltt}
				\highlight{module} examples/tutorial/Map

				\highlight{abstract} \highlight{sig} Object \{\}
				\highlight{sig} Key, Value \highlight{extends} Object \{\}
				\highlight{sig} Map \{ values: Key -> Value \} 
			\end{alltt}
		\end{code}


		As in Java, \highlight{abstract} ensures that there cannot be any direct `instances' of Object. Similarly, 
		\highlight{extends} means that Objects can either be Keys or Values, but not both. \newline


		\emph{values} above is a \emph{relation} that represents the mapping of Keys to Values. 
		This would be written in a schema in Object-Z as \texttt{values} $\subseteq K \times V$ where \texttt{K} is the set of all 
		Keys and \texttt{V} is the set of all Values.


		We can visualize this model as before:


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


		The first instance produced by Alloy only consists of a Key and a Value but no Map. 
		We could browse through the various solutions until we find one that actually 
		includes a Map, however there is a better way. \newline


		As mentioned before, Alloy produces instances that satisfy the 
		predicate passed to \highlight{run}. We can add a constraint that specifies that 
		there is at least one Map: 


		\begin{code}
			\begin{alltt}
				\highlight{pred} show() \{ #Map > 0 \} 
				\highlight{run} show \highlight{for} 2
			\end{alltt}
		\end{code}


		We now get 2 Maps and one Value. To get exactly one Map, we can either change the constraint to:

		\begin{code}
			\begin{alltt}
				#Map = 1
			\end{alltt}
		\end{code}

		or we can modify the \highlight{run} command as follows: 

		\begin{code}
			\begin{alltt}
				\highlight{run} show \highlight{for} 2 but \highlight{exactly} 1 Map
			\end{alltt}
		\end{code}


		Next, let us check that the mapping of keys to values is unique. 
		This can be done in Alloy via \emph{assertions}:

		\begin{code}
			\begin{alltt}
				\begin{tabbing}
				\highlight{assert} \=mappingIsUnique \{ \\
       					\> \highlight{all} m:Map, \= k:Key, v, v':Value | \\
               				\> \> k -> v \highlight{in} m.values \highlight{and} \\
					\> \> k -> v' \highlight{in} m.values \\
					\> \> \highlight{implies} v = v' \\
				\}
				\end{tabbing}
			\end{alltt}
		\end{code}

		This says that if a Map m maps a key k to two values v and v' then they must be the same. 
		Note how the relational product operator (``-\ensuremath{>}'') in k -\ensuremath{>} v is used to represent the tuple 
		(k, v) and how m.values is treated as a set of tuples {(Key, Value)}.  \newline


		To check an assertion, we can use the command \highlight{check}. As for \highlight{run}, we have to specify the scope: 

		\begin{code}
			\begin{alltt}
				\highlight{check} mappingIsUnique \highlight{for} 2
			\end{alltt}
		\end{code}

		If we execute this, Alloy searches all possible combinations of at most two objects of each 
		signature for a counterexample that violates the assertion. Since it cannot find 
		one, it tells us that the assertion may be valid. However, if 
		we increase the scope to three, it produces the following:

		\begin{figure}[h]
			\begin{center}
				\includegraphics[width=\textwidth]{Example_2_01.jpg}
			\end{center}
% 			\caption{Map One}
		\end{figure}

		To make this even more obvious, we can ask Alloy to project over 
		Map using the Projection button.

		\begin{figure}[h]
			\begin{center}
				\includegraphics[scale=0.6]{Example_2_02.jpg}
			\end{center}
% 			\caption{Map Two}
		\end{figure}

		We see that a key refers to two values. To fix this, we use the \highlight{lone} keyword that we have already seen: 

		\begin{code}
			\begin{alltt}
				\highlight{sig} Map \{ values: Key -> \highlight{lone} Value \}
			\end{alltt}
		\end{code}

		Now, the assertion holds even if we increase the scope to 15 (say). 
		This produces a much larger coverage than any testcase ever could and 
		gives us a high level of confidence that the assertion may be valid. \newline


		Finally, to make the instances of later steps less verbose, we include the 
		constraint that all keys (and values) belong to some Map:

		\begin{code}
			\begin{alltt}
				\begin{tabbing}
				\highlight{fact} \=\{ \\
					\> \highlight{all} k:Key | \highlight{some} v:Value, m:Map | k -> v \highlight{in} m.values \\
					\> \highlight{all} v:Value | \highlight{some} k:Key, m:Map | k -> v \highlight{in} m.values \\
				\}
				\end{tabbing}
			\end{alltt}
		\end{code}

		Note that, unlike in the Queue example, it makes sense for a key/value to belong to 
		more than one Map. Also observe that the fact above is anonymous; 
		Alloy does not require you to provide a name. \newline


		We have now developed the static aspects of the Map. In the next section we will 
		continue to develop the dynamics of our example.

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

		We now proceed to adding dynamic behaviour to our model. In particular, 
		we define the operation of adding entries to the Map:

		\begin{code}
			\begin{alltt}
				\highlight{pred} put(m, m':Map, k:Key, v:Value) \{ m'.values = m.values + k -> v \}
			\end{alltt}
		\end{code}

		This is very similar to an operation schema in Object-Z: the instances of \texttt{put} consist 
		of the state before(\texttt{m}), inputs(\texttt{v}), state after(\texttt{m'}) and outputs of the operation. 
		As in Object-Z, the convention is to use ' to decorate the state after the operation. \newline


		+ is the set union operator. The above constraint therefore reads as: \newline


		\emph{``The set of values after is equal to the union of the set of values before with the extra mapping from k to v''} \newline


		(Note how \texttt{m.values} is again treated as a set of tuples). We execute this predicate with the usual command:

		\begin{code}
			\begin{alltt}
				\highlight{run} put \highlight{for} 3 \highlight{but} \highlight{exactly} 2 Map, \highlight{exactly} 1 Key, \highlight{exactly} 1 Value
			\end{alltt}
		\end{code}

		Alloy produces the following instance which illustrates the functionality of the put operation:

		\begin{code}
			\begin{alltt}
			\highlight{module} examples/tutorial/Map
			\highlight{abstract} \highlight{sig} Object \{\}
			\highlight{sig} Key, Value \highlight{extends} Object \{\} 
			\begin{tabbing}\highlight{sig} \= Map \{ \\
				\> values: Key -> \highlight{lone} Value \\
			\} \\
			\highlight{assert} mappingIsUnique \{ \\
				\> \highlight{all} \=m:Map, k:Key, v, v':Value | \\
					\> \> k -> v \highlight{in} m.values  \\
					\> \> \highlight{and} k -> v'\= \highlight{in} m.values \\
						\> \> \> \highlight{implies} v = v' \\
			\} \\
			\highlight{pred} put(m, m':Map, k:Key, v:Value) \{  \\
				\> m'.values = m.values + k -> v  \\
			\}\end{tabbing}	\highlight{run} put \highlight{for} 3 \highlight{but} \highlight{exactly} 2 Map, \highlight{exactly} 1 Key, \highlight{exactly} 1 Value
			\end{alltt}
		\end{code}
		
		\begin{figure}[h!]
			\begin{center}
				\includegraphics[scale=0.55]{Example_2_03.jpg}
			\end{center}
% 			\caption{Map Three - State Before}
		\end{figure}

		\begin{figure}[h!]
			\begin{center}
				\includegraphics[scale=0.55]{Example_2_04.jpg}
			\end{center}
% 			\caption{Map Three - State After}
		\end{figure}

		The assertion \texttt{putLocal} checks that \texttt{put} does not change the existing mappings in the set:

		\begin{code}
			\begin{alltt}
				\begin{tabbing}
				\highlight{assert} \=putLocal \{ \highlight{all} m, m': Map, k, k': Key, v: Value | \\
					\> put[m,m',\=k,v] \highlight{and} k != k' \highlight{implies} \\
						\> \>lookup[m,k'] = lookup[m',k'] \\
				\} \\
				\highlight{fun} lookup(m: Map, k: Key): \highlight{set} Value { k.(m.values) }
				\end{tabbing}\end{alltt}
		\end{code}

		\texttt{lookup} is an example of a \emph{function} in Alloy. It uses the . operator to return all values 
		that are associated with the Key \texttt{k} in the Map \texttt{m}, i.e. the set \texttt{\{$v | (k, v)$ in m.values\}}. 
		Note that the arguments to a function are enclosed in square brackets [ ]. This is new in 
		version 4; in older versions of Alloy, they were enclosed in parentheses (). We check that the assertion holds as before:

		\begin{code}
			\begin{alltt}
				\highlight{check} putLocal
			\end{alltt}
		\end{code}

		Alloy informs us that no counter-examples were found. This is also the case if we increase 
		the scope (to 15, say). Confident that our assertion may be valid, we stop here. \newline

		This concludes the tutorial! If you want to see further examples of Alloy in action, look at 
		section: Further Worked Examples. \ref{Further_Worked_Examples}

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

	\section{Alternatives to Alloy}
	\label{Alternatives}

	\subsection{Z \& Object Z}
	As Alloy was heavily influenced by Z, it is only natural to compare the two. \newline


	Z was first developed in 1977\footnote{cf. \cite{mitFAQ}} by Jean-Raymond Abrial at Oxford University. 
	Being both based on logic and set theory, Alloy closely resembles Z. 
	In fact, Alloy can be viewed as a subset of the Z language. \newline


	One of the advantages of Z is that it has a rich mathematical notation making it 
	more expressive than Alloy. However, Alloy is first order making it automatically 
	analyzable, theorem provers in Z are rather more limited. They are automated only 
	up to a point, complex proofs often require guidance from an experienced user. \newline


	The distinct style and notation of schema calculus gives it the ability to support many 
	different idioms. Alloy on the other hand has a pure ASCII notation and requires no special 
	typesetting tools. Writing out schemas can be tedious in comparison to typing a signature on Alloy! \newline


	Overall, Z has had much more widespread use in education and research. Z has already been 
	applied to several large projects including that on the CICS system by IBM and Oxford 
	University\footnote{cf. \cite{jackson06}}. With continuing development and research being done, perhaps Alloy 
	will one day emulate and even surpass Z. 

	\subsection{Object Constraint Language in UML (OCL)}
	The Object Constraint Language(OCL) is the constraint language of UML. It was developed 
	at IBM and ObjecTime Limited and was added to the UML in 1997. Because it was initially 
	designed to be an annotation language for UML class diagrams, it does not include a 
	textual notation for declarations\footnote{cf. \cite{jackson06} p. 312ff.}. Variants of OCL such as 
	\htmladdnormallink{USE}{http://www.db.informatik.uni-bremen.de/projects/USE/}\footnote{http://www.db.informatik.uni-bremen.de/projects/USE/}
	overcome this limitation. \newline


	OCL is based on first-order predicate logic but uses a syntax similar to programming languages 
	and closely related to the syntax of UML. Alloy is similar to OCL, but its creators claim that 
	Alloy has a more conventional syntax and simpler semantics. Alloy is fully declarative, 
	whereas OCL allows mixing declarative and operational elements. The creators of Alloy 
	\htmladdnormallink{argue}{http://sdg.csail.mit.edu/pubs/1999/omg.pdf}\footnote{cf. http://sdg.csail.mit.edu/pubs/1999/omg.pdf}
	that OCL is too implementation-oriented and therefore not well-suited for conceptual 
	modelling though others believe\footnote{cf. http://www.cs.colostate.edu/~bieman/Pubs/GeorgBiemanFranceUMLWrkshp.PDF} that experience can help keep the specification process 
	with OCL at an abstract level. \newline


	Many tools are available supporting OCL such as 
	\htmladdnormallink{Octopus}{http://octopus.sourceforge.net/} and the \newline
	\htmladdnormallink{Eclipse Model Development Tools}{http://www.eclipse.org/modeling/mdt/?project=ocl}.
	Typical features include the interpretation of OCL constraints over test 
	cases and code generation. Some, such as the USE tool mentioned above, support design-time 
	analysis and exhaustive search over a finite space of cases similar to Alloy.

	\subsection{Vienna Development Method (VDM)}
	Vienna Development Method (VDM) is a set of techniques for developing computer systems. 
	It originated from IBM's Vienna Laboratory in the mid-1970s and was developed by Cliff Jones and 
	Dines Bjorner. VDM includes a specification language called VDM-SL (VDM specification language). \newline

	After the development of VDM in the 1970s there were a few tools for checking VDM specifications, but 
	these were mostly informal projects\footnote{cf. \cite{specBox89} p. 2.}. In 1988 Peter Froome developed a tool called SpecBox which 
	was the first industrialised tool for checking VDM specification. SpecBox is used in 
	civil nuclear, railway and security applications. \newline
	
	There are many other tools for checking VDM specification such as IFAD VDM-SL 
	and Centaur-VDM environment\footnote{http://www.vienna.cc/evdm.htm} which is an interactive and graphical tool for VDM. 
	However unlike Alloy these do not provide fully automatic analysis in the style of 
	a model checker. Both Alloy and VDM support object-orientation and concurrency. \newline
	
	Although it is one of the first formal methods in development, it has been refined, 
	standardized and is still widely used in industry by such organisations as British Aerospace Systems \& Equipment, 
	Rolls Royce and Dutch Department of Defence\footnote{http://www2.imm.dtu.dk/courses/02263/F08/Files/DTU\%20VDM\%20Technology\%20in\%20Industry\%202008.ppt}. Alloy is not used as much in industry as VDM.

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

	\section{Test Yourself!} \label{Test_Yourself}
	You can use the following four questions to test your knowledge of what has been explained so far. 
	More exercises and answers can be found in the \htmladdnormallink{Test Yourself!}{http://www.doc.ic.ac.uk/project/2007/271j/g06271j01/Web/test\_yourself.php}
	section of the website\footnote{http://www.doc.ic.ac.uk/project/2007/271j/g06271j01/Web/test\_yourself.php}.
	\subsection{Questions}
	
	\renewcommand{\theenumi}{\alph{enumi}}

	\subsubsection{Sample Question 1 of 4}
		Look at the following code:

	\begin{code}
		\begin{alltt}
			\highlight{abstract} \highlight{sig} Fruit \{\}
			\highlight{sig} Apple \highlight{extends} Fruit \{\}
			\highlight{sig} Orange \highlight{extends} Fruit \{\}
			\highlight{sig} Pear \highlight{extends} Fruit \{\}
			\highlight{fact} \{ \highlight{lone} Apple \}
			\highlight{fact} \{ \highlight{one} Pear \}
			\highlight{pred} show() \{ #Fruit > 0 \}
			// RUN COMMAND
		\end{alltt}
	\end{code}

	\begin{figure}[h!]
		\begin{center}
			\includegraphics[scale=0.8]{Fruit_Q.jpg}
		\end{center}
		\caption{Fruit}
	\end{figure}

	Which of the following commands produce the above instance?

	\texttt{
	\begin{enumerate}
		\item	\highlight{run} show \highlight{for} 4 \highlight{but} \highlight{exactly} 3 Orange 
		\item	\highlight{run} show \highlight{for} 2 \highlight{but} \highlight{exactly} 0 Apple
		\item	\highlight{run} show \highlight{for} 3 \highlight{but} 2 Orange
		\item	\highlight{run} show \highlight{for} 2 \highlight{but} \highlight{exactly} 2 Orange
		\item	none of the above!
	\end{enumerate}
	}

	\subsubsection{Sample Question 2 of 4} \label{Question_Look_Up}
	Look at the following schema, taken from \cite{russo}:

	\begin{figure}[h!]
		\begin{center}
			\includegraphics[scale=0.6]{Store_Q5.jpg}
		\end{center}
		\caption{Store - Software Engineering I - 2008}
	\end{figure}

	Which one of the following is the correct Alloy translation? \newline

	a)\begin{code}\begin{alltt}\begin{tabbing}
			\highlight{sig} Store { store: Word -> Word } \\
			\highlight{sig} Word \{\} \\
			\highlight{fact} \=unique \{ \\
				\>\highlight{all} a: Word | \highlight{all} x,y: Word | \highlight{some} s:Store | \\
				\>x -> \=a \highlight{in} s.store \highlight{and} y -> a \highlight{in} s.store \\
					\>\>\highlight{implies} x = y \\
			\} \\
			\highlight{fact} singleStore \{ \highlight{one} Store \} \\
	\end{tabbing}\end{alltt}\end{code}

	b)\begin{code}\begin{alltt}\begin{tabbing}
			\highlight{sig} Store \{ store: Word -> Word \} \\
			\highlight{sig} Word \{\} \\
			\highlight{fact} \=unique \{ \\
			\>\highlight{all} \=a,x,y:Word | \highlight{all} s:Store | a -> x \highlight{in} s.store \\
			\>\>\highlight{and} \=a -> y \highlight{in} s.store \\
			\>\>\>\highlight{implies} x = y \\
			\}
	\end{tabbing}\end{alltt}\end{code}

	c)\begin{code}\begin{alltt}\begin{tabbing}
			\highlight{sig} Store \{ store: Word -> \highlight{lone} Word \} \\
			\highlight{sig} Word \{\} \\
			\highlight{fact} singleStore \{ \highlight{one} Store \}
	\end{tabbing}\end{alltt}\end{code}

	\subsubsection{Sample Question 3 of 4}
	A tree can be implemented in Alloy as below:

	\begin{code}
		\begin{alltt}
			\begin{tabbing}
			\highlight{sig} \=Tree \{ \\
				\>root: \highlight{lone} Node, \\
				\>successors: Node -> Node \\
			\} \\ \\
			\highlight{sig} Node \{\} \\ \\
			\highlight{fact} notCyclic \{ \\
				\>no n:Node | n \highlight{in} n.^(Tree.successors) \\
			\} \\ \\
			\highlight{fact} binaryTree \{ \\
				\>\highlight{all} \=n:Node | \\
				\>\>#n.(Tree.successors) = 2  \\
				\>\>\highlight{or} #n.(Tree.successors) = 0 \\
			\} \\ \\
			\highlight{fact} allNodesBelongToOneTree \{ \\
				\>// ??? \\
			\} \\ \\
			\highlight{fact} singleMapping \{ \\
				\>\highlight{all} n,x,\=y:Node | \\
					\>\>x -> n \highlight{in} Tree.successors \\
					\>\>\highlight{and} y -> \=n \highlight{in} Tree.successors \\
						\>\>\>\highlight{implies} x = y \\
			\} \\ \\
			\highlight{pred} show() \{\} \\
			\highlight{run} show \highlight{for} \highlight{exactly} 5 Node, 1 Tree
			\end{tabbing}\end{alltt}
	\end{code}

	\begin{figure}[h!]
		\begin{center}
			\includegraphics[scale=0.5]{Tree_Q6.jpg}
		\end{center}
	\end{figure}

	\begin{enumerate}
		\item	Alloy is more expressive than Object-Z
		\item	Theorem provers in Alloy are not fully automatic and often require guidance from the user
		\item	In contrast to Alloy, Object-Z allows you to prove that a model is correct. 
	\end{enumerate}

	\subsubsection{Sample Question 4 of 4}
	Which of the following is a counterexample to the following assertion\footnote{This is an abridged version of an example taken from \cite{tutorial}}? 

	\begin{code}
		\begin{alltt}\begin{tabbing}
			\highlight{sig} \=Node \{ \\
				\>next: \highlight{lone} Node, \\
				\>prev: \highlight{lone} Node \\
			\} \\ \\

			\highlight{sig} Head \highlight{extends} Node \{\} \\ \\

			\highlight{fact} \=exactlyOneHead \{ \\ 
				\>\highlight{one} Head \\
			\} \\ \\

			\highlight{fact} headHasNoPrev \{ \\
				\>\highlight{no} Head.prev \\
			\} \\ \\

			\highlight{fact} prevIsInverseOfNext \{ \\
				\>\highlight{all} n:\=Node \ensuremath{\mid} \\
				\>\>n.next.prev = n \\
			\} \\ \\

			\highlight{assert} acyclic \{ \highlight{no} n:Node \ensuremath{\mid} n \highlight{in} n.\^{}next \} \\
			\highlight{check} acyclic \highlight{for} 5 \\
			\end{tabbing}\end{alltt}
	\end{code}
	
	a) \begin{figure}[h!]
		\begin{center}
			\includegraphics[scale=3]{Question_3_1.png}
		\end{center}
	\end{figure}


	b) \begin{figure}[h!]
		\begin{center}
			\includegraphics[scale=3]{Question_3_2.png}
		\end{center}
	\end{figure}


	c) \texttt{None. The assertion is valid}
	

	%--------------------------------------------------------------
% 	\subsection{Answers}
% 	These are the answers
% 
% 	\renewcommand{\theenumi}{\alph{enumi}}
% 	\renewcommand{\labelenumi}{\theenumi}
% 
% 	\subsubsection{Answer 1 of 10}
%   		\textbf{a is correct}. \newline 
% 		Alloy cannot automatically prove that a model is valid in general but can be used to check whether it is correct up to a certain size. As most errors usually already occur in small instances, using Alloy to exhaustively check a finite scope allows us to gain a fair level of confidence in our model.
% 
% 
% 	\subsubsection{Answer 2 of 10}
% 		\textbf{c and d are correct}. \newline
% 		These commands allows us to have at least 2 of each fruit!
% 
% 
% 	\subsubsection{Answer 3 of 10}
% 		\textbf{c is correct}. 
% 
% 	\subsubsection{Answer 4 of 10}
% 		\textbf{d is correct}
% 
% 	\subsubsection{Answer 5 of 10}
% 		\textbf{c is correct}
% 
% 	\subsubsection{Answer 6 of 10}
% 		\textbf{c is correct} \newline
% 		Just like in the schema, words map to at most one other word and there can only be one store.
% 
% 	\subsubsection{Answer 7 of 10}
% 		\textbf{a is correct} \newline
% 		All nodes are in one tree including the root node.
% 
% 	\subsubsection{Answer 8 of 10}
% 		\textbf{b is correct} \newline
% 		The first solution does not work: If there is a Value v != v' s.t. k -$>$ v is in m.values, then m'.values would map both v and v' to k. This is impossible because of the use of lone in the definition of values. Removing the existing mapping first avoids this problem.
% 
% 	\subsubsection{Answer 9 of 10}
% 		\textbf{c is correct} \newline
% 		Here is an informal explanation: Assume there is a cycle. Then when we traverse the nodes, we will eventually get back to a node that we have already visited. This node cannot be the Head by headHasNoPrev. Also, it cannot be a non-Head node as this would mean that it that has two prevs. As a node can have at most one prev, this shows that there cannot be a cycle.
% 
% 	\subsubsection{Answer 10 of 10}
% 		\textbf{b is correct} \newline
% 		The quantifier lone means at most one and some means one or more. p has to be drawn from nonempty subsets of X and F must hold.


	%--------------------------------------------------------------
	\renewcommand{\theenumi}{\arabic{enumi}}

	\section{Final Thoughts}
	\label{Final_Thoughts}

	Building our knowledge of Alloy on top of our existing experience of Object-Z was intuitive. 
	With hindsight, we believe not having prior knowledge of Object Z would not have made learning 
	Alloy much more difficult. The ASCII based synthax makes for easy reading and unambigious models. \newline


	Using the Alloy Analyzer was straight-forward and the visualisation feature really helped our 
	understanding. Nothing about the GUI is over-complex and compatibility across Linux, 
	Mac OS and Windows is very good. The fully automated analysis feature is really helpful, 
	instant feedback on your model makes learning more efficient. \newline
	

	The main disadvantage is that Alloy is not used very widely (yet) which can make it hard to find answers 
	to very specific questions. Solutions to most issues are addressed in \cite{jackson06} 
	and addressed by the official (and our!) website! Also, there is a 
	\htmladdnormallink{discussion group}{http://tech.groups.yahoo.com/group/alloy-discuss/}\footnote{http://tech.groups.yahoo.com/group/alloy-discuss/}
	which is unfortunately closed: you have to ask for moderator approval to be able to access it! \newline
	

	In our opinion, Alloy is a great starting point for beginners to specification languages 
	because of its interactive tool support. We think that we would have preferred learning 
	Alloy over Object-Z. \newline
