Playing a bit with Alloy

I have been looking up to Hillel for his great work introducing me and more people into the world of formal specification and verification. Recently he has published yet another great project, Alloydoc:

Hillel

@hillelogram

Want to learn Alloy? Know Alloy but occasionally forget stuff? I wrote a full online reference! alloy.readthedocs.io

You can read the announcement here: hillelwayne.com/post/alloydocs/

16:28 PM - 13 Apr 2020

47 135

Congratulations to Hillel! And to all of us fans. In accord with the advice given in his announcement, I started with the tutorial, during which I decided to have a bit more fun.

I downloaded Alloy from the official source, and typed in the first part of the first code sample, about a file system:

sig FSObject { parent: lone Dir }

sig Dir extends FSObject { contents: set FSObject }

sig File extends FSObject { }

fact { all d: Dir, o: d.contents | o.parent = d }

fact { File + Dir = FSObject }

one sig Root extends Dir { } { no parent }

Here we have four signatures and two facts. Signatures are hopefully obvious: they define sets of objects with fields. If you come from OO world, replace sig with class.

Fact is also often called "invariant" in academic speak. It is a property of the system which must be true at all times. On one hand, you can take the facts for granted when you add new features; on the other hand, you have to be careful not to break the system by breaking the facts. In most languages the compiler cannot reason about the facts, so they are only documented, leaving it for programmers to enforce. Alloy is made to reason about the facts, so we tell Alloy them.

The one and { no parent } in the signature of Root are short-hands to state facts associated with only one signature. one means there is only one Root (singleton), while no parent means the Root has no parent. Straightforward enough I hope.

There were more facts in the tutorial, but I wanted to see what happens if I turn some of them into assert. An assertion is a property which emerges from the signatures and facts. It also must be true for the system to work, but it is like the property of a finished cake, while the facts are like the properties of flour and cream.

The fact in the tutorial is:

fact { FSObject in Root.*contents }

This fact states that all FSObject is either under Root or under Root.contents or under Root.contents.contents and so on. I thought that the above facts and signatures are enough for this to be asserted. So I turn it into:

assert hasContent { FSObject in Root.*contents }
check hasContent for 5

Am I right? No! The check gives me the result:

**Executing "Check hasContent for 5"**
   Solver=sat4j Bitwidth=4 MaxSeq=5 SkolemDepth=1 Symmetry=20
   1003 vars. 62 primary vars. 1441 clauses. 16ms.
   Counterexample found. Assertion is invalid. 11ms.

The Counterexample is a link in the analyzer app, and clicking it opens a nice visualization of the counter example.

File has parent Dir, but Dir doesn't have content File. Dir has parent Root, Root has content Dir. File is FSObject but is not under Root.content chain, so it makes the assertion wrong.

What if I add the fact that all FSObject is in the contents of its parent?

fact { all o: FSObject, d: o.parent | o in d.contents }

**Executing "Check hasContent for 5"**
   Solver=sat4j Bitwidth=4 MaxSeq=5 SkolemDepth=1 Symmetry=20
   1049 vars. 62 primary vars. 1512 clauses. 23ms.
   Counterexample found. Assertion is invalid. 14ms.

File has parent Root, and Root has contents File. But Dir is besides them, not contents of anything, so it makes the assertion wrong.

In hindsight the counter examples are really simple, but before checking I did not catch them.

Alloy is really fun! Modeling in it aligns very well with traditional Object-Oriented concepts as well as relational database concepts. It is great for revealing those false assumptions you hold unconsciously. A logic debugger, if I may. Debug your logic with it when you are stuck!