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

> Alloy Analyzer version 6을 다루는 책.

[Alloy Analyzer](https://wiki.g15e.com/pages/Alloy%20Analyzer.txt) version 6을 다루는 책.

https://practicalalloy.github.io

## Structural modeling

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

### Advanced: Commands in detail

https://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.