用語集（Glossary）
本書で頻出する専門用語・略語を、参照しやすい形でまとめます。定義は「本書での用法（最小）」を優先し、厳密な差分が必要な場合は付録A/付録Cや一次情報を参照してください。
0) 略語（Acronyms）
- SAT：命題充足可能性問題（Satisfiability）。Alloy等が内部で利用することがある。
- SMT：充足可能性の判定を、等式/算術/配列などの理論と統合して扱う枠組み（Satisfiability Modulo Theories）。
- LTL / CTL：時相論理（Linear Temporal Logic / Computation Tree Logic）。模型検査で性質を記述する。
- CI：継続的インテグレーション（Continuous Integration）。PR/夜間/リリース前の検証ゲートに利用する。
- RMW：Read-Modify-Write。並行実行で競合（lost update）を生む典型パターン。
A
Alloy：軽量形式的手法の代表的なツール。関係中心のモデリング言語と反例探索器から構成される。→第4章
アサーション（Assertion）：成立すべき性質を表明する文。Alloyでは assert、プログラム検証では実装上のチェック点として用いる。→第4章/第10章
B
BDD（Binary Decision Diagram）：論理関数を効率的に表現するデータ構造。シンボリック模型検査で使用される。→第8章
C
CSP（Communicating Sequential Processes）：並行システムを、プロセスと通信の合成として表現する枠組み。→第6章
CTL（Computation Tree Logic）：分岐時間論理の一種。到達性や分岐の性質を表現する。→第8章
カリー・ハワード対応：命題と型、証明とプログラムが対応するという見方。→第9章
D
デッドロック：複数のプロセスが互いに待機し合い、進行できない状態。→第6章/第8章
F
不変条件（Invariant）：常に成り立つべき性質。模型検査では反例として破れ方が示される。→第3章/第7章/第8章
公平性（Fairness）：活性を論じる際の前提条件。スケジューリングの仮定が過強だと「見かけ上成立」になり得る。→第7章
H
Hoare論理：プログラムの正しさを推論するための論理体系。事前条件・プログラム・事後条件の三項組で表現する。→第10章
Hoare三項組：{P} S {Q} の形式。Pが事前条件、Sがプログラム、Qが事後条件。→第10章
L
LTL（Linear Temporal Logic）：線形時間論理。時間の流れに沿った性質を表現する。→第7章/第8章
ループ不変条件：ループ実行中に常に成り立つ条件。部分正しさ/完全正しさの証明に使用する。→第10章
M
模型検査（Model Checking）：システムの状態空間を探索し、性質の成立可否を自動判定する手法。→第8章
S
安全性（Safety）：「悪いことが起きない」性質。不変条件として表現されることが多い。→第8章
活性（Liveness）：「良いことがいつか起きる」性質。過度な前提（公平性）に依存しやすい。→第8章
SPIN：Promela言語による並行システムの模型検査ツール。→第6章/第8章
状態空間（State Space）：システムが取りうる状態の集合。状態爆発が主要課題。→第8章
状態爆発問題：状態数が指数的に増大して検証が困難になる問題。→第8章
T
TLA+：分散・並行システムを状態遷移と時相論理で記述する仕様言語。→第7章
TLC：TLA+仕様の模型検査器。→第7章/第8章
トレース（Trace）：状態遷移の列。反例はトレースとして提示される。→第8章
Z
Z記法：状態ベースの形式仕様記述言語。スキーマで状態と操作を表現する。→第5章