How to squeeze all the work you put in your models? Introduce some formality into it! Formal modelling means turning your models into actual artifacts which can be then checked and explored using a tool. This makes is easier to figure out invariants, check the consistency of the whole model, and make clear with each change to the model how it would affect the rest of the system.

This session introduces lightweight formal modelling using Alloy as the tool of choice. We shall explore how to model data — the usual concern in domain modelling — but also how we can describe the possible changes in the system, which ties nicely with ideas such as domain events and commands. A bit of time is also devoted to explain how parts of this executable model can be encoded using formal verification, the natural next step in formality.

To prepare for this lab:

1. Obtain a Java Virtual Machine if don’t have one: java.com/download
2. Download Electrum: github.com/haslab/Electrum2/releases
3. Ensure the Jar you’ve downloaded runs: java -jar electrum-2.1.jar

Trainer and Software Engineer @ 47 Degrees Twitter LinkedIn Company Website

Alejandro is currently a trainer and sofware engineer at 47 Degrees, a company specialized in functional programming. Before that, we was a PhD and lecturer at Utrecht University, working on compilers for functional languages. He has written two books, “Practical Haskell” and “The Book of Monads”, and it’s active in promoting functional programming and Haskell in particular.