This post assumes:

  • you already know that you want to learn some Alloy. That means I will not try to convince you that formal methods are useful or that you should study Alloy. Examples I will use are small and easy to follow as opposed to demonstrating the full power of the tool
  • you haven’t written a single line of Alloy and don’t have anything installed. You start from zero, and therefore I will cover installation and the basics

There are a few Alloy tutorials on the web, but they do not sufficiently explain the basics. For example, all of them skip the installation step. Out of my frustration at the lack of entry-level material, I decided to write this tutorial.

The core parts of this tutorial are videos. I included installation instructions and all code snippets in the text itself to make it easier for you to copy-paste them. At the end of the article you can find links to interesting resources.

Why video? Even though, as a recipient, I prefer to study technical content in text form, I think in the case of Alloy it might be easier to explain things with video. The first reason is that Alloy Analyzer, the only way to use Alloy except of Java API, is a GUI program. Another reason is that result of running Alloy specification is usually a sequence of diagrams. You need to learn how to interpret those to be able to work with Alloy effectively. I believe video can be useful in that regard.

I am an Alloy beginner myself. Thus the code I write might be not idiomatic and my explanations might be superficial. On the other hand, it puts me in a good position for writing beginner’s tutorial as I know what I was struggling with.

Installation

  1. Go to https://github.com/AlloyTools/org.alloytools.alloy/releases and download the latest release. At the moment of writing this guide it’s 5.1.0 and it’s the version I used for recording.
  2. To start Alloy Analyzer GUI run: java -jar org.alloytools.alloy.dist.jar

Part 1: Alloy basics

Link to the video: video

Link to the code: code

Part 2: Static modelling with Alloy

Link to the video: video

Link to the code: code

Initial code for Einstein’s Riddle: code. It contains some basic definitions but you need to encode all the clues as predicates to find the solution.

Next parts - to be done?

Recording first two parts was time consuming endeavour and I decided to stop right here, for some moment at least. I may record next parts one day.

Where to go next

If you are interested with learning more than it was covered in the videos then you have a few options:

  • Tutorial for Alloy Analyzer 4.0 - it covers similar material as the videos, although it does not explain how to install Alloy Tools, work with it and interpret generated examples. If you went through my videos you should be able to follow all the examples easily
  • Software Abstractions book by Alloy’s creator - Daniel Jackson. When buying it pay attention whether you are getting revised edition from 2012. Unfortunately, revised edition is available only in hardcover and its availability may depend on your location. Therefore, I ended up with Kindle version, which is original 2006 edition.
    Regardless of all those logistical issues in getting it, if you become serious about learning Alloy you will need to read this book for sure. It’s very well written and explains design considerations in depth. Similarly to other resources though, it does not explain too much about using GUI itself
  • AlloyDocs by Hillel Wayne. This resource has been published quite recently and as it states it aims to be a reference as opposed to tutorial

Motivational resources

Those may interest you if you wonder why you should even care:

These videos made me realize that formal methods do not need to revolve around costly code verification. Instead, with a small initial investment, you can do design verification and use formal methods as a vehicle for exploring your domain. Something similar in spirit to DDD, UML, or working on a problem at a whiteboard with colleagues.

By the way, Hillel Wayne also writes a fascinating blog in which, among other things, he writes on Alloy, TLA+ and empirical Software Engineering.

Real-world applications of modeling with Alloy