TL;DR
構造的なモデリングに特化した形式仕様言語と、その解析ツールである。MIT の Daniel Jackson 氏が開発した。リレーションロジックに基づいて、システムの静的な構造と制約を記述できる。
なぜ必要か
形式手法のうちモデル検査の道具として使い、設計の段階で仕様の矛盾や抜けを見つけられる。Alloy の特徴は次のとおりである。
- 宣言的に記述する
- リレーション（関係）を中心にモデルを組み立てる
- 仕様に反する例（反例）を自動で生成する
- 小さなスコープの範囲で網羅的に検証する
Alloy 6 は Alloy 4 から大きく改訂され、可変な状態と時相論理が加わった。
仕組み
基本構文
- Signature（
sig）: エンティティを定義する - Multiplicity（多重度）: 関係の数を制約する
- Constraint（制約）: ビジネスルールを定義する
- Quantifiers（量詞）: 条件の範囲を指定する
- 論理演算:
and、or、not、implies、iff - 集合演算:
in、+、&、-、~、^
問題の見つけ方
Assertion（表明）で、成り立つべき性質を検証する。Run コマンドでは問題のあるシナリオを探す。どちらも Alloy Analyzer で実際に実行できる。
インストール
Homebrew で入れられる。
$ brew install --cask alloy例
AI エージェントと組み合わせた活用事例がある。
関連
- 形式手法
- TLA+
- Z 言語
- 抽象によるソフトウェア設計－Alloyではじめる形式手法－: 唯一の日本語の本