付録C 記法対照表
C.1 記法統合ガイド
形式的手法では、複数の記法体系が使用されます。この付録では、本書で扱った主要な記法の対照表を提供し、記法間の対応関係と使い分けのガイドラインを示します。
C.2 基本論理記号
C.2.1 命題論理
| 意味 | 数学記法 | Z記法 | Alloy | TLA+ | 説明 |
|---|---|---|---|---|---|
| 論理積 | ∧ | ∧ | && | /\ | AND演算 |
| 論理和 | ∨ | ∨ | || | \/ | OR演算 |
| 否定 | ¬ | ¬ | ! | ~ | NOT演算 |
| 含意 | → | ⇒ | => | => | ならば |
| 同値 | ↔ | ⇔ | <=> | <=> | 必要十分条件 |
C.2.2 述語論理
| 意味 | 数学記法 | Z記法 | Alloy | TLA+ | 説明 |
|---|---|---|---|---|---|
| 全称量化 | ∀ | ∀ | all | \A | すべての |
| 存在量化 | ∃ | ∃ | some | \E | 存在する |
| 一意存在 | ∃! | ∃₁ | one | - | 唯一存在する |
C.3 集合演算
C.3.1 基本集合演算
| 意味 | 数学記法 | Z記法 | Alloy | TLA+ | 説明 |
|---|---|---|---|---|---|
| 包含 | ⊆ | ⊆ | in | \subseteq | 部分集合 |
| 真部分集合 | ⊂ | ⊂ | - | \subset | 真の部分集合 |
| 和集合 | ∪ | ∪ | + | \cup | 合集合 |
| 積集合 | ∩ | ∩ | & | \cap | 共通部分 |
| 差集合 | \ | \ | - | \ | 差集合 |
| 補集合 | ∁ | ¬ | ~ | - | 補集合 |
C.3.2 集合構成
| 意味 | 数学記法 | Z記法 | Alloy | TLA+ | 説明 |
|---|---|---|---|---|---|
| 内包表記 | {x | P(x)} | {x : S | P • x} | {x : S | P} | {x ∈ S : P} | 条件を満たす要素の集合 |
| 空集合 | ∅ | ∅ | none | {} | 空の集合 |
| 全体集合 | U | U | univ | - | 全要素の集合 |
C.4 関係と関数
C.4.1 関係演算
| 意味 | 数学記法 | Z記法 | Alloy | TLA+ | 説明 |
|---|---|---|---|---|---|
| 関係合成 | R ; S | R ∘ S | R.S | - | 関係の合成 |
| 逆関係 | R⁻¹ | R~ | ~R | - | 関係の逆 |
| 反射閉包 | R* | R* | *R | - | 反射的推移閉包 |
| 推移閉包 | R⁺ | R⁺ | ^R | - | 推移閉包 |
C.4.2 関数記法
| 意味 | 数学記法 | Z記法 | Alloy | TLA+ | 説明 |
|---|---|---|---|---|---|
| 全関数 | f: A → B | f: A → B | f: A -> B | f ∈ [A → B] | 全域関数 |
| 部分関数 | f: A ⇀ B | f: A ⇸ B | f: A ⇸ B | f ∈ [A ⇸ B] | 部分関数 |
| 単射 | f: A ↣ B | f: A ↣ B | - | - | 一対一関数 |
| 全射 | f: A ↠ B | f: A ↠ B | - | - | 上への関数 |
| 全単射 | f: A ↔ B | f: A ⤖ B | - | - | 一対一対応 |
C.5 状態と操作
C.5.1 状態記法
| 概念 | Z記法 | Alloy | TLA+ | 説明 |
|---|---|---|---|---|
| 状態スキーマ | State | sig State | State == … | 状態の定義 |
| 不変条件 | Invariant | fact | TypeOK | 常に成立する性質 |
| 初期状態 | InitState | pred init | Init | 初期状態の定義 |
C.5.2 操作記法
| 概念 | Z記法 | Alloy | TLA+ | 説明 |
|---|---|---|---|---|
| 操作スキーマ | Op | pred op | Next | 状態変化の記述 |
| 事前条件 | pre Op | - | ENABLED Op | 操作の前提条件 |
| 事後条件 | post Op | - | - | 操作の結果条件 |
| フレーム条件 | ΞState | - | UNCHANGED vars | 変化しない変数 |
C.6 時間と時相論理
C.6.1 時相演算子
| 意味 | CTL | LTL | TLA+ | 説明 |
|---|---|---|---|---|
| 常に | AG p | G p | □ p | すべての時点で成立 |
| いつか | AF p | F p | ◇ p | いつかは成立 |
| 次に | AX p | X p | p’ | 次の状態で成立 |
| まで | A[p U q] | p U q | p ∪ q | pがqまで成立 |
C.6.2 TLA+特有記法
| 記法 | 意味 | 説明 |
|---|---|---|
| [A]_v | A ∨ (v’ = v) | Aが成立するか変数vが不変 |
| ⟨A⟩_v | A ∧ (v’ ≠ v) | Aが成立し変数vが変化 |
| WF_v(A) | □◇⟨A⟩_v ∨ □◇¬ENABLED⟨A⟩_v | 弱公平性 |
| SF_v(A) | □◇⟨A⟩_v ∨ ◇□¬ENABLED⟨A⟩_v | 強公平性 |
C.7 記法選択のガイドライン
C.7.1 用途別推奨記法
| 用途 | 推奨記法 | 理由 |
|---|---|---|
| データ構造の仕様 | Z記法 | 豊富な数学記法、詳細な仕様記述 |
| システム設計の検証 | Alloy | 軽量、高速な検証、視覚的なモデル |
| 並行システム | CSP/TLA+ | プロセス記述、時相性質の表現 |
| プロトコル検証 | TLA+ | 分散システム、時間的性質 |
| 要求仕様 | 自然言語+Z | 可読性と厳密性のバランス |
C.7.2 記法習得の順序
- 基礎段階: 基本論理記号、集合演算
- 応用段階: 関係、関数、状態記述
- 発展段階: 時相論理、並行性
- 統合段階: 複数記法の使い分け
C.7.3 記法変換の指針
- Z記法 → Alloy: 状態スキーマをシグネチャに変換
- Alloy → TLA+: 静的構造を動的仕様に拡張
- 自然言語 → 形式記法: 段階的形式化
C.8 実践的記法選択
C.8.1 プロジェクト特性による選択
| プロジェクト特性 | 推奨記法 | 選択理由 |
|---|---|---|
| 高い安全性要求 | Z記法 + 定理証明 | 数学的厳密性 |
| 迅速な検証が必要 | Alloy | 高速な自動解析 |
| 分散システム | TLA+ | 並行性とタイミング |
| レガシー統合 | CSP | プロセス間通信 |
| 教育目的 | Alloy | 学習コストの低さ |
C.8.2 チーム能力による選択
| チーム特性 | 推奨アプローチ | 配慮事項 |
|---|---|---|
| 数学的背景が強い | Z記法中心 | 表現力を活用 |
| プログラマー中心 | Alloy中心 | シンタックスの親しみやすさ |
| 混合チーム | 段階的導入 | 学習曲線の考慮 |
| 初心者チーム | 軽量形式手法 | 成功体験の積み重ね |
この記法対照表は、形式的手法の実践において、適切な記法選択と記法間の変換を支援するためのリファレンスです。プロジェクトの特性とチームの能力に応じて、最適な記法組み合わせを選択してください。