Alloy
https://alloytools.org/
https://zenn.dev/szktty/articles/property-list-model-verification
構造的モデリング に特化した 形式仕様言語
Daniel Jackson 氏（MIT）により開発された
リレーションロジック に基づいてシステムの静的な構造と制約を記述できる
特徴
宣言的 記述
リレーション中心
自動的な 反例 生成
小さな スコープ での 網羅性 検証
インストール（Homebrew）
code:sh
$ brew install --cask alloy
参考になりそうなサイト集
公式
https://alloytools.org/spec.html
非公式
https://alloy.readthedocs.io/en/latest/index.html
https://blog.nekoport.com/
https://qiita.com/kannkyo/items/0742253aeb5a43e449c9
基本構文の要素
Signature（sig）: エンティティ の定義
Multiplicity（多重度）: 関係の数を 制約
Constraint（制約）: ビジネスルール の定義
Quantifiers（量詞）: 条件の範囲を指定
論理演算: and, or, not, implies, iff
集合演算: in, +, &, -, ~, ^
問題発見の仕組み
Assertion（表明）: 成り立つべき性質の検証
Run コマンド: 問題のあるシナリオを探す
Alloy Analyzer で実際に実行できる
AIと共に進化する開発手法：形式手法と関数型プログラミングの可能性
https://gyazo.com/6ccc5221003900355497cd1fa5689a1a
活用事例
Devin + ADR
https://zenn.dev/loglass/articles/2d48f39c3e6424#形式手法（alloy）で仕様をドキュメント化する
Cursor
https://zenn.dev/loglass/articles/5e24364ef06aa9
書籍
抽象によるソフトウェア設計－Alloyではじめる形式手法－（唯一の日本語本）
https://qiita.com/kannkyo/items/0742253aeb5a43e449c9
https://zenn.dev/szktty/articles/property-list-model-verification
#形式手法