Playing a bit with Alloy
Tags: alloy, formal, spec
Published: 2020-04-14 20:35:06

I have been looking up to [Hillel](https://twitter.com/hillelogram) 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](https://alloy.readthedocs.io):

{% twitter 1249736257539911681 %}

Congratulations to Hillel! And to all of us fans. In accord with the advice given in his [announcement](https://www.hillelwayne.com/post/alloydocs/), I started with [the tutorial](https://alloytools.org/tutorials/online/index.html), during which I decided to have a bit more fun.

I downloaded Alloy from [the official source](https://github.com/AlloyTools/org.alloytools.alloy/releases), and typed in the first part of the first code sample, about a file system:

```alloy
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:

```alloy
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:

```alloy
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.](https://i.imgur.com/0QSJelZ.png)

`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`?

```alloy
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.](https://i.imgur.com/7iDCuFE.png)

`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!