なぜ Alloy か

設計文書の多くは、意図は伝わるのに、次の3つで詰まります。

1. 曖昧さ — 「全員に一意の担当者がある」のように、自然言語では解釈の余地が残る
2. 境界の抜け — 例外や「ありえない」経路の見落とし
3. 主観的な合意 — コードレビューで「たぶんこう」に依存する

Alloy（言語）と Alloy Analyzer（ツール群）は、小さな設計案を、制約として書き、機械的に解や反例を探すのに使います。全コードを形式検証する、という意味ではなく、仕様の骨格を点検する用途が中心です。

自然言語と Alloy モデル

要するに、曖昧な文を、関係と制約に置き換えて問い直す道具です。

このブックの読み方

1. まず 5分で価値を体験 で、ツール上で「解が出る／出ない」が何を意味するか触る
2. 最初のモデル 以降で、表現力を少しずつ足す
3. 画面のボタン名は Alloy Analyzer の UI 用語 に合わせる

次は インストールが未なら インストール、済みなら 5分で価値を体験 へ進んでください。