Practical Alloy: A hands-on guide to formal software design

Alloy Analyzer version 6을 다루는 책.

practicalalloy.github.io

Structural modeling

practicalalloy.github.io/chapters/structural-modeling/index.html

Advanced: Commands in detail

practicalalloy.github.io/chapters/structural-topics/topics/commands/index.html

Sometimes we want to encode negative run commands to show that a certain class of instances is disallowed, or invalid check commands to register some known issues. We could use comments to annotate which is the case, but Alloy allows the user to register what is the expected outcome of a command using a keyword expect after the scope declaration.