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.
- 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.
- 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
Links and References
Those may interest you if you wonder why you should even care:
- Tackling Concurrency Bugs with TLA+ by Hillel Wayne
- Finding bugs without running or even looking at code by Jay Parlar
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
- Using Lightweight Modeling To Understand Chord - a classic paper in which Pamela Zave shows that Chord protocol do not hold guarantees it stated it holds
- A Practical Comparison of Alloy and Spin by Pamela Zave
- The Same-Origin Policy - Eunsuk Kang et al., a chapter of The Architecture of Open Source Applications
Other interesting links
- Use of Formal Methods at Amazon Web Services by Chris Newcombe et al.
- An Empirical Study on the Correctness of Formally Verified Distributed Systems by Pedro Fonseca et al. It’s an amazing paper, one of the very few empirical studies on the correctness of verified systems and it helps to understand the place of formal methods in the bigger picture of delivering software
- Alloy meets TLA+: An exploratory study by Nuno Macedo, Alcino Cunha