はじめに
このブックは、Alloy という形式手法向けのモデリング言語と、Alloy Analyzer（AlloyTools が配布するツール群）の使い方を、インストールから一通りの操作まで段階的に追えるようにまとめたものです。
読み方の骨格は次の通りです。まず「なぜ Alloy か（設計で得られる価値）」、続けて短い体験で操作と結果の意味を掴み、そのうえで言語と Analyzerの基礎に入ります。いきなり構文の細部から入らず、腹落ちしながら進められる構成にしています。
このブックでできるようになること
- Alloy Analyzer を自分の環境に導入し、起動できる
- 小さなモデルを書き、満たすインスタンスの探索や 命題の検査 を実行できる
- GUI（エディタ・Visualizer）と、配布に含まれる CLI の基本を理解する
- さらに学ぶための一次情報へ進める
想定する読者
- プログラムや設計の仕様を、曖昧さを減らして書きたい人
- 形式手法に興味はあるが、どのツールから入るか迷っている人
- 既存の英語リソース（例: Practical Alloy）とあわせて、日本語で導入のレールが欲しい人
執筆上の注意（バージョン）
Alloy 6 系の構文とツール差分に依存する箇所があります。2026 年 4 月時点で GitHub の最新安定リリース は Alloy 6.2.0（2025-01-09 公開）です。新しい版が出たら、次を正としてください。
乖離を見つけた場合は、本リポジトリへの指摘を歓迎します。
用語
- Alloy: 言語そのもの
- Alloy Analyzer: ソルブや可視化を行う中心ツール（本書では alloytools.org の配布物 に沿って説明します）
次の章
- Alloy を設計でどう活かすか、まだイメージが薄い方は なぜ Alloy か から。
- すでに導入の動機はある方も、上記章は短いので一読推奨です。
- そのあと インストール へ進み、起動できたら 5分で価値を体験 です。