About this Presentation
	Overview of the Alloy Language
	Using Alloy and the Alloy Analyzer
	Summary
	Quiz (Donuts!)
	Q & A
Overview of Alloy
	What is Alloy?
		Modelling language based on first-order logic
		Heavily inspired by Z (Schemas!)
		Z is not easily analyzable
		Alloy tries to overcome this
		Has to sacrifice some of Z's power to be able to do so
	Scope: Z > Alloy > Test Cases
		Z can be used to prove correctness
		Alloy Analyzer allows automatic verification within a finite scope
		Relies on Small Scope Hypothesis
		[Picture Test Case vs. (finite) assertion]
Using Alloy and the Alloy Analyzer: The Example
	Computer: a collection of components
		Harddisk
		CPU
		Memory
	Example extremely simple
	Full power of Alloy can be seen better still on bigger examples
Alloy in Real Life
	Example just given was very simplistic
	Alloy has been used for much more complex systems, eg:
		Cryptography
		Document Structuring
		Railway Switching
	Taught at many universities around the world
Summary
	Alloy is a modelling language inspired by, but less powerful than Z
	However, in contrast to Z, it is automatically analyzable
	The Alloy Analyzer allows visualizing instances of models and checking assertions within a finite scope
	This makes it easy to incrementally explore design ideas
	In our opinion, Alloy is a good starting point for beginners to specification languages
Further Resources
	Alloy Website
	Our Website
	Software Abstractions by Daniel Jackson
Quiz
	Question 1 from the Website

Q&A