付録A：数学的基礎の復習

本付録は、本書で頻出する数学記法の最小セットを「参照用」にまとめます。厳密な講義ノートではなく、本文（第4章Alloy、第5章Z、第6章CSP、第7章TLA+）の読解と仕様記述のためのチートシートです。

記法は、同じ概念でも流派・ツールで差が出ます。本書内での表記ゆれを避けるため、詳細は付録C（記法対照表）も参照してください。

A.1 集合（Set）

集合は「要素の集まり」を表します。仕様記述では、状態や許容される値の集合を表す基本単位です。

よく使う記号：

要素所属：x ∈ A（x は A の要素）、x ∉ A
部分集合：A ⊆ B（A は B に含まれる）、A ⊂ B（真部分集合）
空集合：∅
集合演算：A ∪ B（和集合）、A ∩ B（積集合）、A \ B（差集合）
冪集合：ℙ X（X の部分集合全体）
直積：X × Y（順序対の集合）
濃度（要素数）：#A

例：

A = {1, 2, 3}
B = {3, 4}

1 ∈ A
A ∩ B = {3}
A \ B = {1, 2}

A.2 論理（Logic）

仕様の制約は、論理式で表します（不変条件、事前条件、事後条件など）。

接続詞（命題を組み合わせる）：

否定：¬P（not P）
連言：P ∧ Q（P and Q）
選言：P ∨ Q（P or Q）
含意：P ⇒ Q（P ならば Q）
同値：P ⇔ Q（P と Q は同値）

量化（「すべて」「存在」を表す）：

全称量化：∀x : X • P(x)（X のすべての x について P(x)）
存在量化：∃x : X • P(x)（X のある x が存在して P(x)）

例（「全口座の残高は非負」）：

∀a : Account • balance(a) ≥ 0

A.3 関係と写像（Relation / Function）

関係は「2つの集合の要素の対応」を表します。写像（関数）は、その特別な場合です。

関係（relation）

関係 R は、X × Y の部分集合として考えられます：

R ⊆ X × Y

Z記法では、型として次を用います：

R : X ↔ Y（X と Y の間の関係）

よく使う演算：

定義域：dom R（X側の現れる要素）
値域：ran R（Y側の現れる要素）

写像（function）

写像（関数）は「入力ごとに出力が一意に定まる」関係です。

本書では、次を最小セットとして用います：

全関数：f : X → Y（X のすべての要素に対して値が定義される）
部分関数：f : X ⇸ Y（一部の要素では未定義でもよい）

例（期限が設定されていない本もある）：

dueDate : Book ⇸ Date

A.4 状態・操作・不変条件（State / Operation / Invariant）

仕様では、状態（state）と操作（operation）を分離して記述します。

最小の見取り図：

状態：システムが保持するデータ（集合・関係・写像）
不変条件（invariant）：常に成り立つべき制約
操作：状態を更新する手続き（事前条件/事後条件、フレーム条件）

例（銀行口座の制約の概念図）：

状態: balance : Account → Int
不変: ∀a : Account • balance(a) ≥ 0
操作: withdraw(a, amount)
  事前: amount > 0 ∧ balance(a) ≥ amount
  事後: balance'(a) = balance(a) - amount

A.5 同値関係と帰納法（必要最小）

同値関係（equivalence relation）

同値関係 ~ は、次の3性質を満たす関係です：

反射律：∀x • x ~ x
対称律：∀x, y • x ~ y ⇒ y ~ x
推移律：∀x, y, z • x ~ y ∧ y ~ z ⇒ x ~ z

同値関係は「同じものとして扱う」単位（同値類）を作るときに使います（識別子、正規化、抽象化など）。

帰納法（induction）

帰納法は、自然数や列（ステップ）に沿って性質を示す基本技法です。最小形は次の2段です：

基底：P(0) を示す
帰納：P(n) ⇒ P(n+1) を示す

状態遷移の議論では、「nステップ目まで成り立つ」→「n+1ステップでも成り立つ」の形で、不変条件を説明する際の補助線になります。