Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

はじめに

このブックは、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分で価値を体験 です。

なぜ Alloy か

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

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

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

自然言語と Alloy モデル

自然言語の例モデル上で起きること（イメージ）
ユーザーは1つの組織にだけ属する多対一の関係として書く。反例を探して矛盾を出す
転送中は一時的に二重所有あり得る時間や状態を導入し、不変条件（欲しい性質）を check する

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

このブックの読み方

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

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

インストール

Alloy Analyzer は Java ランタイム 上で動作する配布物（JAR）や、OS 向けのパッケージとして提供されます。入手先は Download および GitHub Releases です（latest が常に最新の安定版です）。

1. Java の確認

ターミナルで次を実行し、Java が入っているか確認します。

java -version

Alloy 6 系では、公式 README でも Java 17 以降の JVM が前提とされています。java -version で満たない場合は Eclipse Temurin 等で入れてください。

2. 配布物の取得

次のいずれかを選びます。

  • JAR 単体: どの OS でも共通。java -jar org.alloytools.alloy.dist.jar のように起動する。
  • OS 用アーカイブ（.zip / .tar.gz 等）: 同梱スクリプトで起動しやすい。macOS では .dmg や aarch64 / amd64 の違いに注意。

リリース資産名は版ごとに変わるため、必ず対象リリースの README を読んでファイルを選んでください。

3. 起動の確認

起動方法は配布物に依存します。典型例:

java -jar org.alloytools.alloy.dist.jar

GUI のウィンドウが開き、空のエディタが表示されれば、まずは成功です。メニュー表記はバージョンで多少異なる場合があります。

4. バージョンの固定（推奨）

学習の途中で挙動が変わるのを防ぐため、特定のリリースに固定して進めるのがおすすめです。本ブックの例は Alloy 6 系を想定しています。確認時点の安定版は 6.2.0 ですが、常に 最新リリース の番号を正としてください。自分の環境のバージョン（About 相当の画面や、同梱 CLI の help 等）をメモしておくとトラブル時に便利です。

次の章

まず 5分で価値を体験 で、Analyzer 上の操作と結果の意味を掴みます。すでに Alloy を触ったことがある人も、Execute / Show という画面語で手順を揃え直す意味で読んでください。終わったら 最初のモデル へ。

5分で価値を体験

前提: Alloy Analyzer を起動 できること。

この章のゴール

  • ソースに書かれた run / check を、ツール上では Execute で実行し、結果を Show で見る
  • SAT/UNSAT（または同様の結果表記）を、「設計上、ありうる/矛盾している」に読み替えられる

手順

  1. New で新規。エディタに下を貼り、Save（保存）する。
sig Item {}
one sig Inventory {
  contains: set Item
}
pred someItems {
  #Inventory.contains > 0
}
run someItems for 3

assert allItemsListed { all i: Item | i in Inventory.contains }
check allItemsListed for 3

check 側の例は、「宇宙にいる Item はみな在庫 contains に入っている」と主張する、という解釈にしています。Item の一部だけが在庫に載っている世界を許す run の解では、この主張は成り立たないことが多く、反例（反証となるインスタンス）が出やすいです。
量化了な i を本文（i in ...）で必ず使う形にしてあり、未使用変数のコンパイラ警告が出ないようにしてあります。

  1. ツールバーから Execute（実行）— 上から順に、デフォルトで定義した run / check が走る動きを想定。実際の既定順は版で違うことがある。まず run 相当が選ばれていることを確認（メニューでコマンドを切り替えられる版もある）。
  2. 結果（解あり/なし 等）を確認し、Show（あるいは Visualizer/Theme へ進む導線）でインスタンスを眺める。
  3. 同じく Execute で check 側（assert）を走らせ、反例が出るか/出ないかを見る（版によって「次の解」「どの断片を走らせるか」の操作が違います。迷ったら Alloy Analyzer の操作）。

何が得られたか

  • 例がある（run が満たす解を示す）= 想定世界が一つは成り立つ、という具体例
  • 性質に反例がある（check）= 制約の書き方と意図が食い違う、という手がかり
  • どちらも、議論の「たぶん」に対する手触りになる

用語の対照は Alloy Analyzer の UI 用語 を参照。次は 最初のモデル で、小さなドメインを一緒に式にします。

最初のモデル

この章で得ること

  • 何を式として切り出すか（sig や関係＝設計の境界）の感覚
  • run が「ありうる世界の具体例を探す」操作であること
  • ツール上では Alloy Analyzer の UI 用語 の Execute / Show を使い、結果を読むところまで踏む

目標

  • シグニチャ（集合のような表現）とフィールド（関係）を最小限書く
  • run で 解を探索 する
  • 結果を Analyzer 上で確認する

例: 本と著者

次の例は、本と人、そして「誰が著者か」という関係を表す最小モデルです。同じ内容は、サイト上では examples/hello.als（リポジトリ直下では examples/hello.als）からも開けます。

sig Book {}
sig Person { wrote: set Book }
pred show {}
run show for 3

ざっくり説明

  • sig は集合の枠。ここでは Book と Person があります。
  • wrote は Person から Book への関係（誰がどの本を著者とみなすか）です。set Book なので、著者 0 冊以上を持てます。
  • pred は述語。ここは空の show です（あとで拡張してもよい）。
  • run show for 3 は、大きさ 3 までの範囲でインスタンスを探す、という趣旨（厳密な解釈は Analyzer の表記に従います）。

手元で試す

  1. Analyzer を起動する。
  2. 上のコードを新規ファイルに貼り、.als として**Save** する（未保存のまま Execute しても期待どおりに動かないことがあります）。
  3. ツールバーから Execute して、モデルに書かれた run 相当をソルバに渡す（版によってはメニューで run / check のどれを先に走らせるか選びます。迷ったら Alloy Analyzer の操作）。
  4. 見つかったインスタンスを Show や Theme / Visualizer で眺める（用語の対照は Alloy Analyzer の UI 用語）。

run が UNSAT（解なし）になった場合、制約を強めすぎていないか、for のスコープが狭すぎないか、を疑うとよいです。

check の入口

run は「ある制約付きモデルの存在」を探し、assert に対する check は「常に成り立つか」をソルブで検査します。最初は run だけ使えれば十分です。

次の章

言語の基礎 で、リレーションと制約の表現力を少し押さえます。

言語の基礎

この章の制約（多重度、fact、assert 等）は、設計上こういう問いに答えるための表現です。「この関係の形は許されるか？」「想定する不変条件は常に成り立つか？」を、小さなスコープの宇宙で手触りを確かめながら進めてください。画面のボタン名と run / check の対応は Alloy Analyzer の UI 用語 を参照。

リレーションと多重度

Alloy の中心は関係です。フィールド f: A -> B は、A の元と B の元の対応（任意の多対多）を表せます。set / lone / one / some 等多重度は、この対応の形に制約を与えます。

制約

fact { ... } には、常に成り立たせたい事実を置きます。pred や assert とは使い分けの違いがあれど、探索（run） では pred をゴールにし、検査（check） では不変条件を assert に残す、という分け方が扱いやすいです。check を走らす画面操作は、GUI では Execute（結果はビルド表記の SAT/UNSAT 等。版依存）に対応します。対照表は Alloy Analyzer の UI 用語 を参照。

量化子

all, some, no, lone など、一階述語の量化がそのまま使えます。まず小さい宇宙（for のスコープ）で、成り立つ / 成り立たないのスケッチを見比べると学習が速いです。

モジュール

open util/... など、標準ライブラリの利用を前提にしつつ、自分の module 分割はモデルが大きくなった段階で導入すれば十分です。

次の章

Alloy Analyzer の UI 用語 で用語の対照を押さえたうえで、Alloy Analyzer の操作 で、ソルブの読み方と Visualizer、CLI への入口を扱います。

Alloy Analyzer の UI 用語

方針: 手順の本文では、画面のラベル（下表「このブックの呼び方」）を使う。コード断片内の run / check など言語キーワードはそのまま。

主なツールバー（例: Alloy 6.2.0 付近の GUI）

このブックの呼び方ざっくり役割補足
New新しいモデル
Openファイルを開く
Reload再読み込み
Save保存手順不整合の多くは未保存が原因
Executeモデルに書かれた run / check 等をソルバに渡す版で「何を最初に走らせるか」は異なる。メニューで対象を選べる版も
Showインスタンスやグラフ表示系へ版で Visualizer/Theme との違いを確認

画面語と Alloy 言語

画面で行う操作の内容ソース上の用語（例）
具体例（世界）を探すrun（述語）
性質が常に成り立つかassert + check
インスタンスの探索範囲for スコープ（例: for 3）

版差: メニュー名が「Run」「Build」等に違う場合は、手元の表示を正とし、本ブックの表は「意味の地図」として読んでください。乖離を見つけたら リポジトリ へ指摘歓迎です。

Alloy Analyzer の操作

この章で得られること

  • 何が分かるか: ソースの run / check をソルブに渡した結果（SAT/UNSAT や同様表記。版依存）を、制約付き世界の有無/性質の反例の有無に読み替える
  • どう触るか: 画面操作は、まず Alloy Analyzer の UI 用語 の New / Save / Execute / Show など、ラベルで辿る（run という述語と、Run という英単語のボタン名を取り違えない）
  • 次に行く道: 非対話的な実行・CI には 実務への接続 を次の一歩として用意している

エディタと Execute（run / check の実行）

  • コンパイル（エラーチェック）: エディタ上で構文・型のエラーを直す。直さない限り Execute は意図どおりに進みません。
  • ソルバの実行: モデルに run や check などのコマンドが定義されているとき、Execute によってソルブを走らせ、SAT（解あり）/ UNSAT（制約不整合）/ 有界完了 などの結果を読みます。表記の細部は版で異なります。

ソース上の キーワード run / check のまま会話に含めてよい一方、手順では「Execute を押し、定義した run 相当（または check 相当）を走らせる」と書くと、スクリーンショット上の用語と揃います。

インスタンスと Show / Theme

インスタンス（見つかった解）を、Show や Theme、表形式のビューで追うと、関係の形が掴みやすいです。大きいモデルでは、投影して見る、スコープを下げる、制約を分解する、といった切り方が有効です。

Visualizer

グラフや表の見え方の切替、ハイライト、レイアウトの調整など、直観の補助に使います。版によってメニュー名は変わるため、手元のヘルプと照合しながら慣れましょう。ここに進む導線は、版によって Show から繋がるか、Visualizer として別名になっているかが異なります。

CLI と LSP

Alloy 6.2.0 のリリースノートでは、配布 JAR に コマンドライン（例: java -jar <配布 jar> help でヘルプ）と LSP サーバ（起動オプション lsp）が記載されています。実際のサブコマンド名・オプションは、手元の help 出力と リリースノート を正としてください。

CI でモデルを走らせる、スクリプト化する、エディタ連携を試す、といった運用上の詳細手順の置き場所は、本書では重複を避け 実務への接続 に委ねます。入門本編の GUI 用語表は、引き続き Alloy Analyzer の UI 用語 を正とします。

  1. PATH に CLI を通す、または java -jar で JAR を直接呼ぶ
  2. オプションで入力ファイル、出力形式、解の個数、時間制限等を与える（help に従う）
  3. 失敗（退出コード）を CI に載せる

OS ごとのパスやファイル名は、JAR 配布か OS パッケージかで変わります。配布物の README を正とし、どのバイナリ（または JAR）が alloy 相当かをインストール先で確認してください。

困ったとき（最小のトラブルシュート）

  • Save したか — 手順が期待どおりに動かない多くは、未保存や別ファイルを見ているのが原因です。Save してから Execute。
  • スコープが狭すぎないか — for 3 等が厳しすぎると、意図した反例や解を見落とすことがあります。まず上げ下げを試す。
  • 制約が強すぎないか — 一度に詰め込まず、fact を外す／assert を弱める、と分割してどこで UNSAT になるかを切り分ける。

次の章

可変性とトレース（Alloy 6） では、状態と時間の扱いの入口に触れます。

可変性とトレース（Alloy 6）

本編では時間と状態の入り口に立つ章です。先に 言語の基礎 と Alloy Analyzer の操作（必要なら Alloy Analyzer の UI 用語）を済ませておくと、トレースの読み方がつかみやすいです。

Alloy 6 では、可変な状態や実行のトレースを扱う表現が強化され、より「振る舞い」の探索に近づけます。一次情報は Alloy 6 の紹介 と ドキュメント を参照してください。

何のための章か

  • ある初期状態から遷移の列を探索し、仕様が意図した通りかを見る
  • 不変条件がトレース全体で保たれるかを check で押さえる

学び方のすすめ

  1. まず小さな 遷移システム（数行の sig と pred）で run し、Visualizer で列として見る
  2. util/ordering など、標準ライブラリの慣用に慣れる
  3. スコープを上げる前に、遷移の長さや状態の大きさを分けて調整する

このブックでは入り口のみ示し、本文の深掘りは公式資料と Practical Alloy 等へ委ねます。

次の章

演習 で手を動かしましょう。

演習

用語の注意: 本書のソースコード中では run / check という言語の用語をそのまま使います。一方、画面の手順では Alloy Analyzer の UI 用語 の Execute 等に合わせてください。

解答の方針は 一つではありません。まず 解が出るか / 反例が出るか を確認し、そのあとで制約を絞り込む、という順が学習には向きます。

1. 著者は少なくとも一人

examples/hello.als（またはリポジトリの examples/hello.als）を出発点に、すべての本に少なくとも一人の著者がいることを fact で表現し、run で解が得られることを確認してください。

ヒント: Book 全体に対する all 量化と、wrote の逆方向の関係を考えます。

2. 著者は高々一人

同じモデルで、各本の著者は高々一人（重複著者なし）を追加したとき、意図した挙動になるかを確認してください。check で性質を書いても、run で反例を探しても構いません。

3. CLI（余力）

インストールした配布物の CLI で、上記のいずれかのファイルを非対話的に実行し、CI に載せるイメージを掴んでください。オプション名は版固有情報のため、手元の --help を正としてください。

次の章

次の一歩 へ。

実務への接続

この章の位置づけ: 入門を終えたあと、チームでどう続けるかの地図だけ示す。深掘りは各公式ドキュメントへ。

手段できること入門者が次に取る一歩（例）
CLI（配布 JAR 同梱）同じ .als を非対話的に実行、スクリプト化手元の help 出力でサブコマンドを1つ通す。CI に載せるイメージは 演習
LSPエディタで診断・定義等（版による）好みのエディタの Alloy 拡張有無を調べ、Analyzer と同じ配布のドキュメントを正とする
CI検査の再現と共有リポジトリに .als を置き、ビルドで JAR 実行1本にする（詳細はチーム方針）

初版のスコープ: 詳細手順の多数提示は行わない。常に alloytools.org とリリースノートを正とする。

次: 次の一歩 で公式学習リソースを選ぶ。

次の一歩

入門完了のチェックリスト

  • 3 分で説明できる: Alloy / Analyzer を設計に持ち込むと、何が得られるか（曖昧さの削減、反例、具体例の探索）
  • 画面語で辿れる: 少なくとも Save / Execute / Show 相当の何を指しているか、自分の手元の版で言える
  • 一文で言える: run と check の違い（具体例の探索 / 不変条件の検査）と、それが設計上のどの問いに答えるか
  • 一歩次へ: 公式ドキュメントか 実務への接続 のどこか一つに、次に何をするかを決めている

目的別

  • 学習: 本書の 演習 と、英語で掘り下げるなら Practical Alloy を併用する
  • 研究: 公式 ドキュメント と Alloy 6 概要 から、扱う時間・可変性の表現に合わせる
  • チーム導入: CI・CLI・LSP の導入イメージは 実務への接続 を出発点にし、配布物の help とリリースノートを正にする

公式一次情報

学習用の本（英語）

コミュニティ

講演資料や論文、周辺ツール（LSP 等）の状況は移り変わります。最新は 公式サイトとリリース を併せて追うのが安全です。

このリポジトリへ

誤字・不整合・よりよい演習案は、Issue / PR で歓迎します。book.toml の git-repository-url や site-url を、あなたのフォーク先に合わせて更新したうえで、変更を送ってください。