付録C：記法対照表
本付録では、形式的手法で頻出する用語・記号の最小セットと、AI時代のDoDチェックリストをまとめます。
C.1 用語集（Glossary）
- invariant（不変条件）：常に成り立つべき性質。反例が出たら仕様/実装の破綻を示す。
- safety（安全性）：悪いことが起きない性質（例：二重引き落としが起きない）。
- liveness（活性）：良いことがいつか起きる性質（例：要求がいつか処理される）。
- refinement（詳細化）：抽象仕様から実装仕様へ段階的に具体化する手続き。
- contract（契約）：事前条件/事後条件を明文化した実行時/検証時のガード。
- trace（トレース）：状態遷移の列。反例はトレースとして提示される。
- counterexample（反例）：性質が破れる最小の実行例。設計修正の入口。
C.2 AI時代のDoDチェックリスト
AI支援開発では、出力の正当性を検証器で担保することが前提です。
- 仕様差分がある場合、対応する形式仕様も更新されている
- 検証ログに seed/深さ/スコープ/実行コマンドが含まれている
- 反例が出た場合、修正履歴と再検証ログが残っている
- 例外承認の理由・代替策・フォローアップ期限が明記されている
C.3 記法対照表（Z / Alloy / CSP / TLA+）
以下は「同じ概念」を各記法でどう表現するかの最小対応表です。章内の表記（第4章Alloy、第5章Z、第6章CSP、第7章TLA+）と整合する範囲で記載します。
コードブロックのラベル：
- ツール準拠（そのまま動く）：そのままツール/CLIへ貼り付けて実行できることを意図した記法（環境差により追加設定が必要な場合あり）。
- 文脈依存スニペット：構文自体は実ツールに沿うが、前提となる宣言・モデル・ハーネス・対話コンテキストを別途必要とする断片。
- 擬似記法：説明用に数学記法・省略表記・出力例等を含む記法（ツール入力としての厳密性を保証しない）。
注意：
- ツール準拠（そのまま動く）のコードフェンス内には、ツール入力として有効な文字列のみを記載する（出力例・図示・自然言語説明は入れない）。
- 変数宣言・
MODULE main・検証ハーネス・対話コンテキストなど、周辺の必須要素を別の場所に置く場合は 文脈依存スニペット を使う。 - 周辺の必須要素を本文や参照先で明示している断片は 文脈依存スニペット、参照先を明示していない断片や数学記法・省略・自然言語を含む断片は 擬似記法 として扱う。
- 図示/出力例/擬似コードは 擬似記法 を使用する。
C.3.1 概念の対応（最小セット）
| 概念 | Z記法（本書） | Alloy（Alloy Analyzer 6想定） | CSP（本書/ツール） | TLA+（TLC想定） |
|---|---|---|---|---|
| 集合（型） | A : ℙ X |
A: set X |
事象集合 {a, b} / 同期集合 X |
A ∈ SUBSET X |
| 要素所属 | x ∈ A |
x in A |
（事象）a ∈ X |
x ∈ A |
| 関係 | R : X ↔ Y |
R: X -> Y |
（通常は直接は書かない） | R ⊆ X × Y |
| 全関数 | f : X → Y |
f: X -> one Y |
（通常は直接は書かない） | f ∈ [X -> Y] |
| 部分関数 | f : X ⇸ Y |
f: X -> lone Y |
（通常は直接は書かない） | （必要なら部分関数として表現） |
| 状態 | 状態スキーマ | 時刻（ステップ）を明示してモデル化 | プロセス（状態は遷移に埋め込む） | 変数 v と次状態 v' |
| 初期状態 | InitState |
pred Init[...] |
初期プロセス P0 |
Init == ... |
| 遷移/操作 | ΔState |
pred Step[s, s'] |
前置 a → P（ツールでは a -> P） |
Next == ... |
| 不変条件（安全性） | スキーマ制約 | fact / assert |
refinement / assertions（ツール依存） | Invariant == ... / []P |
| 活性/公平性 | （拡張が必要） | （トレース上で表現） | （ツール依存） | <>P, WF_vars(A), SF_vars(A) |
注記：
- Zの
↔/→/⇸/↦は第5章の記号体系に合わせています。 - CSPは本文では数学記法として
→, □, ⊓を用い、ツール（FDR/CSPM）では代表的に->, [], |~|を用います。
C.3.2 Z記法：主要記号（読みの目安）
| 記号 | 意味 | 読み（例） |
|---|---|---|
ℙ X |
冪集合 | power set of X |
x ∈ A |
要素所属 | x is in A |
R : X ↔ Y |
関係 | relation from X to Y |
f : X → Y |
全関数 | (total) function from X to Y |
f : X ⇸ Y |
部分関数 | partial function from X to Y |
x ↦ y |
maplet（ペア） | x maps to y |
dom R, ran R |
定義域/値域 | domain/range |
C.3.3 Alloy：主要記号（Alloy Analyzer 6）
| 記号 | 意味 | 例 |
|---|---|---|
sig / フィールド |
集合と関係 | sig User { files: set File } |
多重度 one/lone/some/set |
要素数制約 | owner: one User |
fact |
常に成り立つ制約 | fact { ... } |
assert + check |
性質検証（反例探索） | check Inv for 5 |
run |
充足例探索 | run { ... } for 5 |
. / ~ / ^ |
結合/転置/推移閉包 | u.files, ~r, ^parent |
C.3.4 CSP：主要記号（本文/ツール）
| 概念 | 本書表記（数学記法） | ツール表記（CSPM/FDRの代表例） |
|---|---|---|
| 前置（prefix） | a → P |
a -> P |
| 外部選択 | P □ Q |
P [] Q |
| 内部選択 | P ⊓ Q |
P |~| Q |
| 同期並行（同期集合X） | P [| X |] Q |
P [| X |] Q |
| インタリーブ | P ||| Q |
P ||| Q |
| 隠蔽（hiding） | P \ X |
P \\ X |
| リネーム | P[[ a ← b ]] |
P[[ a <- b ]] |
注記：ツール表記は代表例です。プロジェクトでは使用ツール（FDR版、CSP dialect）に合わせて確認してください。
C.3.5 TLA+：主要記号（TLC）
| 記号 | 意味 | 例 |
|---|---|---|
v' |
次状態の値 | x' = x + 1 |
[]P / <>P |
常に / いつか | []Inv, <>Goal |
WF_vars(A) / SF_vars(A) |
公平性仮定 | WF_vars(Next) |
.cfg |
TLC設定 | 初期状態/不変条件/探索制約 |
補足：
- Alloyは有限範囲の反例探索が中心。状態遷移を扱う場合は、時間（ステップ）を明示してモデル化する
- TLA+は状態遷移と時相論理が中心。実装詳細を詰める前に、高レベルで性質（不変/活性）を固定する
- Zは状態/操作（スキーマ）で要件を厳密化し、実装へ詳細化する