\chapter{Conclusion \& Evaluation}
\section{Conclusion}
We have developed a website that introduces undergraduate students familiar with first-order logic and Object-Z to the structural modeling language Alloy and its Analyzer. In this report, we have given the contents of the website, an additional larger example showing how Alloy can be used to solve puzzles and an overview of the technologies used and decisions made. To conclude our project, we will now give our personal experience of the technologies used throughout the project, an account of Alloy as a teaching tool and an outlook on how the website could be used and expanded upon in the future.

\section{Personal Experience of the Technologies used}

\subsection{HTML}
This was the first language we looked at for writing our webpage in. Whilst it is simple and easy to learn, we found formatting in HTML can be quite difficult. Using CSS improved formatting significantly and made for uniform style across all our pages.

\subsection{JavaScript}
We made limited use of JavaScript to increase accessibility, as some browsers have it disabled. We did find it useful in certain applications such as disabling the Submit button in the ``Test Youself'' section and to open a new window for the Flash demo. We found JavaScript straight-forward to learn and use however spotting errors is hard because some browsers do not give you feedback when there is a JavaScript error.

\subsection{PHP}
Our knowledge of object oriented programming gave us a good foundation for learning PHP. There is a very large and active PHP developer community online which was helpful when we ran into problems. Learning and using PHP was simple and provided us with a quick and efficient way of organising the website.

\subsection{LaTeX}
LaTeX offers an efficient way of formatting the contents of a document. Having worked with HTML and CSS the principles of Latex were easy to grasp. We found the seperation between content and design enabled us to write the report in a formal fashion seamlessly.

\subsection{Demo Builder}
Having already worked with Adobe Flash, Demo Builder was extremely simple to learn and intuitive to use. It enabled us to create the introductory video to Alloy's user interface on the website in a few hours (that is, from downloading and learning Demo Builder to the completion of the final version ov the video). We believe that creating such a movie cannot be made much easier and highly recommend Demo Builder (its website is http://www.demo-builder.com).

\subsection{Alloy}
As already stated in section \ref{Final_Thoughts}, learning Alloy on top of our existing experience with first-order logic, Object-Z and programming was very easy. This was helped very much by the Alloy Analyzer which is itself intuitive and simple to use. In addition, the Official Alloy tutorial (http://alloy.mit.edu/alloy4/tutorial4) was of great help, as was Daniel Jackson's book Software Abstractions.

\subsection{Alloy as a Teaching Tool in Comparison to Object-Z}
We have seen in section \ref{Alternatives} that while Alloy may look like it is less mathematical than Object-Z, the two are actually very similar. Like Alloy, Z (and thus Object-Z since it is an extension of Z) is at heart just a logic, augmented with some syntactic constructs to make it easy to describe software abstractions. In Z, schemas are used to encapsulate both declarations and constraints. \newline

In Alloy, declarations are packaged into signatures while constraints are encapsulated in functions, facts and predicates. Schemas can be refined and extended using schema inclusion in Z. The same can be achieved in Alloy using the signature extension mechanism. Class Schemas in Object-Z are a bit more powerful than signatures in Alloy because they provide constructors. \newline

Therefore, even though an Alloy model might look less mathematical than an Object-Z model, in reality the differences between the two languages are minor. For teaching purposes, we thus believe that the distinguishing factor does not lie within their syntax or semantics but in the tool support available. \newline

The most notable tool supporting Z/Object-Z seems to be the Community Z Tools project CZT (http://czt.sourceforge.net/) that can be used standalone on the command line or as a plugin to jEdit/Eclipse where it provides automatic code completion, type checking etc. It comes with a command line, \emph{textual} tool called ZLive that provides an animator for evaluating Z expressions, predicates and schemas and is intended to be used for interactively testing a model. CZT seems to be well suited for people experienced in using Z/Object-Z; however it is by far not as user friendly and intuitive as the Alloy Analyzer. \newline

Also, in our opinion, the one feature that can help someone learning a modelling language the most, being able to visualize instances of a model, is implemented in the Alloy Analyzer far better than in CZT. Because the underlying theoretical concepts are nearly identical, that is why, from our limited perspective as students, we think that Alloy would be a good alternative to Object-Z for introducing undergraduate students to formal specifications.  

\subsection{Outlook}
Alloy offers a lightweight approach to formal specifications which fits well with the ongoing move away from heavyweight methods and the increasing popularity of Agile methodologies in software engineering. It is hard to tell whether it will become used widely; it might not seem rigorous enough to purists and not worth the effort to software engineers. However, we believe that Alloy, even if it does not become an industrial standard, is very suitable for introducing undergraduate students to formal specifications. \newline

In its current state, the website we have developed can be used to introduce students who have a background in Z/Object-Z to Alloy. For example, it might be as a starting point for a student project that uses Alloy. In the future, the website might be enhanced in the following ways:

\begin{description}
	\item[More General Audience] The website currently requires some knowledge of formal specifications. It could be expanded to address a more general audience. 
	\item[Browser Compatibility] The website was only designed for Mozilla's Firefox web browser and can look quite different on other browsers (eg in Microsoft Internet Explorer). This could be fixed. 
	\item[Conformance with Web Standards] Many minor aspects of the website such as specifying ``alt''-attributes for images, making links underlined so they stick out to people with color vision deficiencies etc. could be improved(cf. http://www.maxdesign.com.au/presentation/checklist.htm). 
\end{description}
