形式的手法の基礎と応用

第2章　数学とプログラムの橋渡し

2.1 プログラミングに潜む数学的構造

「数学は苦手だけど、プログラミングは好き」という人は多いのではないでしょうか。しかし実は、プログラミングの行為そのものが、既に高度に数学的なのです。あなたが変数を宣言し、関数を定義し、条件分岐やループを書くとき、無意識のうちに数学的な概念を使っています。

この事実に気づくことが、形式的手法への第一歩です。形式的手法は、プログラミングの延長線上にある技術であり、全く新しい世界ではありません。既にあなたが知っている概念を、より明示的に、より厳密に表現する方法なのです。

本章では、プログラミングの基本概念と数学的概念の対応関係を明らかにし、第3章以降で学ぶ形式仕様記述への自然な橋渡しを行います。特に、第4章のAlloyモデリング、第5章のZ記法、第6章のCSP、第7章のTLA+で使用する数学的基盤を、既知のプログラミング概念から導入していきます。

図2-1: プログラミング概念と数学概念の対応関係

変数という名前の数学的対象

プログラミングで最初に学ぶ概念の一つが「変数」です。しかし、なぜ「変数」と呼ばれているのでしょうか。数学の方程式 y = 2x + 1 の x や y と、プログラムの int count = 0 の count には、どのような関係があるのでしょうか。

実は、両者は同じ数学的概念の異なる表現です。数学の変数が「値の範囲」を表すように、プログラムの変数も「取りうる値の集合」を持っています。int 型の変数は整数の集合から値を選び、boolean 型の変数は真偽値の2要素集合 {true, false} から値を選びます。

より深く考えると、プログラムの実行は「変数に値を割り当てる過程」として理解できます。これは数学的には「関数の定義」に相当します。時刻 t における変数 x の値を x(t) と表現すれば、プログラムの実行は時間の関数として記述できるのです。

この視点は、第7章で学ぶTLA+（Temporal Logic of Actions）の基礎となります。TLA+では、システムの状態を変数の値の組として表現し、状態変化を時間軸上の関数として記述します。また、第10章のプログラム検証では、この「変数の値の変化」を数学的に追跡して、プログラムの正しさを証明する技法を学びます。

関数：入力と出力の関係の抽象化

プログラミングにおける関数は、数学の関数と本質的に同じものです。入力（引数）を受け取り、何らかの処理を行って、出力（戻り値）を返します。数学の関数 f(x) = x² と、プログラムの関数 square(x) { return x * x; } は、表記法は違いますが、同じ概念を表現しています。

しかし、プログラミングの関数には、数学の関数にはない側面があります。「副作用」です。ファイルを読み書きしたり、画面に出力を表示したり、他の変数の値を変更したりすることがあります。この副作用も、実は数学的に記述できます。関数を「システムの状態を変換する操作」として捉えれば、副作用も含めて数学的に表現できるのです。

この状態変換の概念は、第5章のZ記法で中心的な役割を果たします。Z記法では、操作を「事前状態」から「事後状態」への変換として厳密に記述します。また、第10章のプログラム検証では、Hoare論理を用いて、副作用を持つプログラムの正しさを事前条件と事後条件で表現する手法を学びます。

制御構造：論理の具現化

条件分岐（if-then-else）やループ（for、while）も、論理学の概念の具現化です。条件分岐は論理の「含意」に対応し、ループは「再帰的定義」や「帰納法」に対応します。

例えば、以下のような単純な条件分岐を考えてみましょう：

if (age >= 18) {
    status = "adult";
} else {
    status = "minor";
}

これは、論理学的には以下のように表現できます： 「年齢が18以上ならば成人、そうでなければ未成年」

この文を数学的に記述すると： status = (age ≥ 18) ? "adult" : "minor"

ループはより複雑ですが、同様に数学的に記述できます。for ループは数列の定義に、while ループは条件を満たす最小値の探索に対応します。

データ構造：集合と関係の実現

配列、リスト、辞書（ハッシュマップ）などのデータ構造も、数学的概念の実装です。配列は「順序付けられた集合」、辞書は「関数」（キーから値への写像）、グラフは「関係」の表現です。

配列 [1, 3, 5, 7, 9] は、数学的には添字の集合 {0, 1, 2, 3, 4} から値の集合 {1, 3, 5, 7, 9} への関数として理解できます。つまり、f(0) = 1, f(1) = 3, f(2) = 5, ... という関数の表現なのです。

連想配列（辞書）はさらに明確です。{"name": "Alice", "age": 30} というデータ構造は、文字列の集合 {"name", "age"} から値の集合への関数です。

このような集合と関数の概念は、第4章のAlloyモデリングで中心的な役割を果たします。Alloyでは、すべてのデータを集合と関係（リレーション）として表現し、システムの構造と振る舞いを記述します。第5章のZ記法でも、状態を変数名から値への関数として表現し、データ構造を集合演算で操作します。

型システム：集合論の実践的応用

プログラミング言語の型システムは、集合論の実践的な応用です。型は「値の集合」を定義し、型チェックは「集合の包含関係」を確認します。

例えば、整数型 int は整数の集合を表し、文字列型 string は文字列の集合を表します。型安全性とは、「関数が期待する型の値のみが渡されることを保証する」ことであり、これは数学的には「関数の定義域を明確にする」ことに相当します。

より高度な型システム（ジェネリクス、代数的データ型、依存型など）は、さらに複雑な数学的構造を扱います。これらは、プログラミングが数学にどれだけ近づけるかを示しています。

エラー処理：例外的状況の数学的表現

プログラムにおけるエラー処理や例外処理も、数学的に表現できます。関数の戻り値を「正常な値または例外」という和型（union type）として捉えれば、エラーも含めて数学的に記述できます。

関数 divide(a, b) を考えてみましょう。この関数は、b = 0 のときは定義されません。数学的には、この関数の定義域は「b ≠ 0 を満たす実数の組 (a, b)」です。プログラムでのゼロ除算エラーは、この定義域外での関数呼び出しに相当します。

2.2 「正しさ」を数学的に表現する

直感的正しさから形式的正しさへ

プログラマーは常に「正しい」プログラムを書こうとします。しかし、「正しい」とは何でしょうか。コンパイルが通ること？期待通りに動作すること？バグがないこと？これらの直感的な理解から、数学的に厳密な「正しさ」の概念を構築してみましょう。

プログラムの正しさは、本質的には「仕様と実装の一致」です。仕様は「プログラムが何をすべきか」を定義し、実装は「プログラムが実際に何をするか」を定義します。正しさとは、これら二つの間の対応関係なのです。

仕様という約束

仕様を理解するために、日常生活のアナロジーを使ってみましょう。料理のレシピを考えてください。レシピは「材料と手順」を指定し、「期待される結果」を記述します。「玉ねぎを炒めて飴色になるまで」「強火で3分間」といった指示は、実は非常に厳密な仕様です。

プログラムの仕様も同様です。「ユーザー名とパスワードを入力として受け取り、認証が成功すればtrueを、失敗すればfalseを返す」といった記述は、関数の入力、出力、振る舞いを定義する仕様です。

しかし、料理のレシピと同じように、自然言語による仕様には曖昧性があります。「飴色になるまで」とは、具体的に何分でしょうか？どの程度の色でしょうか？「認証が成功する」とは、どのような条件を満たすことでしょうか？

数学的仕様の力

数学的仕様は、この曖昧性を排除します。認証関数の仕様を数学的に表現すると：

authenticate: String × String → Boolean
事前条件: username と password は空でない文字列
事後条件: 
  - (username, password) が有効な組み合わせの場合、結果は true
  - そうでない場合、結果は false
  - データベースの内容は変更されない

この記述は、自然言語の記述よりもはるかに明確です。関数の型（入力と出力の種類）、事前条件（関数が正しく動作するために必要な条件）、事後条件（関数が保証する結果）が明示されています。

実装との対応関係

実装は、この仕様を満たすようにコードを書くことです。しかし、「満たす」とは何でしょうか？これが、形式的手法における「適合性」の概念です。

実装が仕様に適合するとは、数学的には以下を意味します：

  1. 事前条件を満たすすべての入力に対して、実装は停止する
  2. 実装の出力は、事後条件を満たす
  3. 実装は、仕様で許可されていない副作用を引き起こさない

この定義は抽象的に見えますが、実は非常に具体的で検証可能です。

部分正しさと全正しさ

プログラムの正しさには、二つの側面があります。「部分正しさ」と「全正しさ」です。

部分正しさは、「プログラムが停止した場合、その結果は正しい」ことを意味します。しかし、プログラムが無限ループに陥ったり、クラッシュしたりする可能性は排除しません。

全正しさは、「プログラムは必ず停止し、その結果は正しい」ことを意味します。これは、部分正しさに「停止性」を加えた概念です。

例えば、以下のような関数を考えてみましょう：

function factorial(n) {
    if (n <= 1) return 1;
    return n * factorial(n - 1);
}

この関数の部分正しさは、「n が自然数の場合、結果は n! である」ことです。しかし、全正しさを保証するには、「n が自然数の場合、この関数は必ず停止する」ことも証明する必要があります。

不変条件：システムの約束

プログラムの正しさを考える上で重要な概念が「不変条件」です。これは、プログラムの実行中に常に成り立つべき性質です。

例えば、銀行口座のシステムでは、「すべての口座の残高の合計は、預金総額と引き出し総額の差に等しい」という不変条件があります。どのような操作を行っても、この性質は保たれなければなりません。

不変条件は、システムの「一貫性」を保証する概念です。データベースの整合性制約、オブジェクト指向プログラミングのクラス不変条件、並行プログラムの同期条件などは、すべて不変条件の例です。

仕様の階層性

実際のシステムでは、仕様は階層的に構成されています。システム全体の仕様、モジュールの仕様、関数の仕様が、それぞれ異なるレベルで定義されます。

この階層性は、複雑性の管理に不可欠です。各レベルで適切な抽象化を行うことで、人間が理解可能な形でシステム全体の正しさを保証できます。

形式的手法は、この階層的な仕様を厳密に記述し、各レベルでの正しさを数学的に証明する技術を提供します。

2.3 集合論：プログラムの世界を記述する言語

データの本質：要素の集まり

プログラムで扱うデータは、本質的には「要素の集まり」です。整数、文字列、オブジェクト、これらはすべて何らかの集合の要素です。集合論は、この「集まり」を厳密に扱うための数学的な枠組みを提供します。

集合論の基本概念は直感的です。集合は「物の集まり」であり、要素は「集合に属する物」です。プログラミングでは、型が集合に対応し、値が要素に対応します。int 型は整数の集合、boolean 型は {true, false} という2要素集合です。

集合演算：データ操作の数学的記述

プログラムでのデータ操作は、集合演算として理解できます。和集合（∪）、積集合（∩）、差集合（\）、これらの演算は、プログラムでの一般的な操作に対応します。

例えば、二つのユーザーグループがあるとき：

  • 管理者グループ：{Alice, Bob, Charlie}
  • 開発者グループ：{Bob, David, Eve}

和集合は「どちらかのグループに属するユーザー」：{Alice, Bob, Charlie, David, Eve} 積集合は「両方のグループに属するユーザー」：{Bob} 差集合は「管理者だけで開発者でないユーザー」：{Alice, Charlie}

これらの操作は、プログラムでのリスト結合、フィルタリング、検索などの操作の数学的記述です。

関係：要素間のつながり

集合論のもう一つの重要な概念が「関係」です。関係は、異なる集合の要素間の対応を表現します。プログラムでの多くの構造は、関係として理解できます。

データベースのテーブルは関係の典型例です。「学生」と「科目」の間の「履修関係」は、数学的には学生の集合と科目の集合の直積の部分集合として表現できます。

学生 = {Alice, Bob, Charlie}
科目 = {数学, 物理, 化学}
履修関係 = {(Alice, 数学), (Alice, 物理), (Bob, 数学), (Charlie, 化学)}

関数：特別な関係

関数は、特別な性質を持つ関係です。各入力に対して、出力がただ一つ決まる関係が関数です。プログラムの関数は、この数学的な関数の実装です。

関数の重要な性質として、「定義域」と「値域」があります。定義域は関数が定義される入力の集合、値域は可能な出力の集合です。プログラムでの型エラーは、多くの場合、定義域外の値を関数に渡すことで発生します。

例えば、平方根関数 sqrt の定義域は非負実数の集合です。負の数を渡すとエラーになるのは、その値が定義域に含まれていないからです。

順序関係：比較と並び替え

プログラムでよく使われる操作の一つが「比較」です。数値の大小比較、文字列の辞書順比較、日付の前後関係など、これらはすべて「順序関係」の例です。

順序関係は、集合の要素間の「順序」を定義する関係です。数学的には、反射的（a ≤ a）、反対称的（a ≤ b かつ b ≤ a ならば a = b）、推移的（a ≤ b かつ b ≤ c ならば a ≤ c）という性質を持つ関係として定義されます。

プログラムでのソートアルゴリズムは、この順序関係を利用してデータを並び替えます。ソートの正しさを証明するには、使用している関係が実際に順序関係の性質を満たすことを確認する必要があります。

カルテシアン積：複合データの構造

複合データ型（構造体、タプル、レコード）は、数学的にはカルテシアン積（直積）として表現できます。二つの集合 A と B のカルテシアン積 A × B は、(a, b) の形の順序対の集合です。

例えば、座標を表すデータ型：

Point = {(x, y) | x ∈ Real, y ∈ Real}

これは、実数の集合の直積 Real × Real です。

より複雑な例として、ユーザー情報：

User = Name × Age × Email
Name = String
Age = Natural
Email = String

このように、複合データ型は基本型の直積として数学的に記述できます。

冪集合：選択肢の集合

集合 A の冪集合 P(A) は、A のすべての部分集合の集合です。これは、プログラムでの「選択肢の集合」に対応します。

例えば、権限システムで、基本権限の集合が {read, write, execute} の場合、可能な権限の組み合わせは冪集合の要素です：

P({read, write, execute}) = {
  {}, {read}, {write}, {execute},
  {read, write}, {read, execute}, {write, execute},
  {read, write, execute}
}

プログラムでのビット演算、フラグの組み合わせ、設定項目の選択などは、冪集合の操作として理解できます。

2.4 論理：プログラムの性質を語る言語

命題：真偽を持つ文

プログラムの世界では、常に何かを判断しています。「ユーザーは認証されているか」「配列の範囲内にあるか」「ファイルは存在するか」。これらの判断は、論理学では「命題」として扱われます。

命題は、真または偽の値を持つ文です。プログラムでの boolean 型の変数や、条件式の結果は、命題の具体的な表現です。命題論理は、これらの命題を組み合わせて、より複雑な条件を表現する方法を提供します。

論理演算子：条件の組み合わせ

プログラムの条件式で使う AND (&&)、OR (   )、NOT (!) は、論理学の論理演算子そのものです。これらの演算子には、数学的に厳密な定義があります。

論理積（AND）: P ∧ Q は、P と Q が両方とも真のときのみ真 論理和（OR）: P ∨ Q は、P または Q の少なくとも一方が真のとき真 否定（NOT）: ¬P は、P が偽のとき真、P が真のとき偽

これらの演算子は、真理表によって完全に定義されます。プログラムでの複雑な条件式も、これらの基本演算子の組み合わせで表現できます。

含意：条件の関係

プログラムロジックで重要な概念の一つが「含意」です。「A ならば B」という関係は、論理学では「A → B」と表記されます。これは、A が真のとき B も真であることを意味します。

プログラムでの条件分岐は、含意の具体的な実装です：

if (user.isAuthenticated()) {
    // ユーザーが認証されているならば、秘密情報にアクセス可能
    return secretData;
}

この条件分岐は、「ユーザーが認証されている → 秘密情報にアクセス可能」という含意を実装しています。

述語論理：より表現力豊かな論理

命題論理だけでは表現できない概念があります。「すべてのユーザーは有効なメールアドレスを持つ」「少なくとも一人の管理者が存在する」といった文は、量詞を使った述語論理で表現する必要があります。

全称量詞（∀）: 「すべての」を表す 存在量詞（∃）: 「少なくとも一つの」を表す

例：

  • ∀x ∈ Users. hasValidEmail(x) : すべてのユーザーは有効なメールアドレスを持つ
  • ∃x ∈ Users. isAdmin(x) : 少なくとも一人の管理者が存在する

この述語論理は、第3章の仕様記述技法で詳しく学び、第4章のAlloyや第5章のZ記法で実際に使用します。第8章の模型検査では、これらの論理式を自動的に検証する技術を扱い、第9章の定理証明では、論理的推論によってより複雑な性質を証明する手法を学びます。

論理と制御構造

プログラムの制御構造は、論理的な構造に対応しています。

条件分岐は含意に対応：

if (condition) { action() }
≡ condition → action()

ループは量詞に対応：

for (item in collection) { process(item) }
≡ ∀item ∈ collection. process(item)

例外処理は排他的論理和に対応：

try { normalAction() } catch { errorAction() }
≡ (normalAction() ∧ ¬error) ∨ (errorAction() ∧ error)

論理的推論：プログラムの証明

論理学の推論規則は、プログラムの正しさを証明するための基礎となります。代表的な推論規則には以下があります：

モダス・ポネンス（前件肯定）:

P → Q, P
---------
     Q

三段論法：

P → Q, Q → R
-------------
    P → R

これらの推論規則を使って、プログラムの性質を段階的に証明できます。

論理的等価性：条件式の最適化

論理学の等価性は、プログラムの条件式を最適化するために使われます。ド・モルガンの法則、分配法則、結合法則などは、条件式を読みやすく、効率的に書き換えるための基礎となります。

ド・モルガンの法則：

¬(P ∧ Q) ≡ (¬P ∨ ¬Q)
¬(P ∨ Q) ≡ (¬P ∧ ¬Q)

プログラムでは：

!(a && b) ≡ (!a || !b)
!(a || b) ≡ (!a && !b)

2.5 状態と変化：動的システムの数学的モデル化

状態という概念の深層

プログラムの実行は、本質的には「状態の変化の連続」です。この「状態」という概念を数学的に厳密に定義することが、動的システムを理解する鍵となります。

状態とは、ある時点でのシステムのすべての情報の完全な記述です。プログラムでは、すべての変数の値、メモリの内容、ファイルシステムの状態、ネットワーク接続の状況など、システムの振る舞いに影響するすべての情報が状態に含まれます。

数学的には、状態は「状態空間」という集合の要素として表現されます。状態空間 S は、システムが取りうるすべての可能な状態の集合です。

状態遷移：変化の数学的記述

プログラムの実行による状態の変化は、「状態遷移」として表現されます。状態遷移は、数学的には状態空間上の関数として定義できます。

遷移関数 δ: S × I → S は、現在の状態 s ∈ S と入力 i ∈ I を受け取り、新しい状態 s’ ∈ S を返します。ここで、I は可能な入力の集合です。

図2-2: 状態遷移モデル（銀行口座システムの例）

例えば、単純なカウンターを考えてみましょう：

状態空間 S = Integer（カウンターの値）
入力集合 I = {increment, decrement, reset}
遷移関数：
  δ(n, increment) = n + 1
  δ(n, decrement) = n - 1
  δ(n, reset) = 0

状態の抽象化：複雑性の管理

実際のプログラムの状態空間は膨大です。現代的なコンピュータでは、64ビットのメインメモリだけで 2^64 通りの状態が可能です。この膨大な状態空間を人間が直接扱うことは不可能です。

そこで重要になるのが「抽象化」です。システムの本質的な性質に影響する状態の要素のみを取り出し、詳細を省略することで、管理可能なサイズの状態空間を作ります。

例えば、Webアプリケーションのユーザーセッションを考える場合：

具体的状態：メモリ内のすべてのバイト値、TCPコネクションの詳細、...
抽象状態：{logged_out, logged_in, admin_session}

この抽象化により、数十億通りの具体的状態を3つの抽象状態で表現できます。

不変条件：状態の制約

すべての状態が有効というわけではありません。システムには、常に満たされるべき性質があります。これが「不変条件」です。

不変条件は、状態空間の部分集合として表現できます。有効な状態の集合を Valid ⊆ S とすると、不変条件は「常に s ∈ Valid である」という性質です。

銀行システムの例：

状態：各口座の残高の組 (balance1, balance2, ..., balanceN)
不変条件：∀i. balancei ≥ 0（すべての口座の残高は非負）

状態遷移の性質

状態遷移には、重要な性質があります：

決定性: 同じ状態で同じ入力を与えれば、常に同じ次の状態になる 全関数性: すべての状態と入力の組み合わせに対して、次の状態が定義されている 部分関数性: 一部の状態と入力の組み合わせでは、次の状態が定義されない（エラー状態）

プログラムの例外処理やエラーハンドリングは、部分関数性を扱うためのメカニズムです。

並行システムの状態モデル

単一プロセスのシステムでは状態遷移は順次的ですが、並行システムでは複数の遷移が同時に発生する可能性があります。これにより、状態モデルは格段に複雑になります。

並行システムの状態は、各プロセスの状態の組み合わせとして表現されます：

S = S1 × S2 × ... × SN

しかし、すべての組み合わせが有効というわけではありません。プロセス間の同期や相互排斥により、実際に到達可能な状態は制限されます。

インターリービング：並行実行の数学的記述

並行システムの実行は、「インターリービング」として理解できます。これは、各プロセスの操作を時間軸上で組み合わせることです。

二つのプロセス P1 と P2 があり、それぞれ操作列 [a, b] と [x, y] を実行する場合、可能なインターリービングは：

[a, b, x, y]
[a, x, b, y]
[a, x, y, b]
[x, a, b, y]
[x, a, y, b]
[x, y, a, b]

この組み合わせ爆発が、並行システムの複雑性の根源です。第6章で学ぶCSP（Communicating Sequential Processes）では、このような並行実行を数学的に記述し、プロセス間の通信と同期を厳密に扱う技法を学びます。第7章のTLA+では、より複雑な分散システムの並行性を時相論理で表現する方法を扱います。

状態空間の探索

形式的手法における検証の多くは、状態空間の探索に基づいています。システムの初期状態から始めて、可能なすべての状態遷移を辿り、到達可能なすべての状態を調べます。

この探索により、以下のような性質を確認できます：

  • 不変条件違反の検出
  • デッドロック状態の発見
  • 特定の目標状態への到達可能性
  • 悪い状態への到達不可能性

時間の扱い：離散と連続

プログラムシステムの時間モデルには、離散時間と連続時間があります。

離散時間モデルでは、時間は自然数の列 {0, 1, 2, …} で表現され、各時点での状態が定義されます。多くのソフトウェアシステムは、この離散時間モデルで十分に表現できます。

連続時間モデルでは、実数の時間軸上でシステムの状態が変化します。リアルタイムシステムや物理シミュレーションでは、連続時間モデルが必要になることがあります。

章末課題

理解確認演習1：データ構造の集合論的表現

以下のプログラムのデータ構造を集合論的に表現してください：

class Student:
    def __init__(self, name, age, courses):
        self.name = name        # 文字列
        self.age = age          # 整数
        self.courses = courses  # 文字列のリスト

students = [
    Student("Alice", 20, ["Math", "Physics"]),
    Student("Bob", 22, ["Chemistry", "Biology"]),
]
  1. Student クラスの型を直積として表現
  2. courses フィールドの型を冪集合として表現
  3. students リストの型を集合として表現
  4. 特定の学生が特定の科目を履修しているかを判定する関係を定義

理解確認演習2：論理と制御構造

以下の自然言語の条件を論理式で表現し、さらにプログラムの条件式として実装してください：

  1. 「18歳以上かつ有効な免許証を持つ場合のみ、運転できる」
  2. 「管理者であるか、またはファイルの所有者である場合、ファイルを削除できる」
  3. 「すべてのユーザーが有効なメールアドレスを持つ」
  4. 「少なくとも一つの商品が在庫切れでない」

実践演習：状態モデリング

単純な自動販売機を状態遷移システムとしてモデル化してください：

機能：

  • 硬貨投入（100円、500円）
  • 商品選択（コーラ150円、お茶100円）
  • キャンセル（投入金額を返却）
  • お釣り計算

要求：

  1. 状態空間を定義
  2. 入力集合を定義
  3. 状態遷移関数を定義
  4. 不変条件を少なくとも3つ特定
  5. 正常な購入シナリオの状態遷移列を示す

発展演習：並行性の分析

以下のような銀行振込システムを考えてください：

Account A: balance = 1000
Account B: balance = 500

Transaction 1: A → B (300円)
Transaction 2: B → A (200円)

両方の取引が同時に実行される場合：

  1. 各取引の状態遷移を定義
  2. 可能なインターリービングをすべて列挙
  3. それぞれの実行結果を計算
  4. 不整合が発生する可能性を分析
  5. 不整合を防ぐための制約を提案

統合演習：形式的手法への準備

以下の演習は、第3章以降で学ぶ形式的手法の基礎を準備するものです：

演習1：Alloyモデリングの準備

Webアプリケーションのユーザー管理システムを以下の観点で分析してください：

  1. エンティティの特定：User, Role, Permission等の基本要素を集合として定義
  2. 関係の記述：「ユーザーが役割を持つ」「役割が権限を持つ」関係を数学的に表現
  3. 制約の形式化：「管理者は少なくとも一人必要」等のビジネスルールを述語論理で記述
  4. 不変条件の特定：システムが常に満たすべき性質を論理式で表現

目標：第4章のAlloyモデリング実習への準備

演習2：Z記法の基礎準備

銀行口座システムの基本操作を状態変換として分析してください：

  1. 状態スキーマ：口座の状態（残高、口座番号等）を変数の集合として定義
  2. 操作スキーマ：預金、引き出し、振込操作を事前条件と事後条件で記述
  3. エラー処理：残高不足等の例外的状況の取り扱いを形式化
  4. 操作の合成：複数の操作を組み合わせた複合操作の記述

目標：第5章のZ記法実践への準備

演習3：CSP並行性の基礎

チャットシステムのクライアント・サーバー通信を分析してください：

  1. プロセス特定：クライアント、サーバー、メッセージキューを並行プロセスとして記述
  2. 通信チャネル：メッセージ送受信の同期通信を数学的に表現
  3. プロトコル設計：ログイン、メッセージ送信、ログアウトの順序制約
  4. デッドロック分析：起こりうる並行性の問題を特定

目標：第6章のCSP並行システム設計への準備

演習4：TLA+時相論理の基礎

分散ファイルシステムの整合性を時間的観点から分析してください：

  1. 状態変数：ファイルのバージョン、レプリカの状態等を時間の関数として定義
  2. 安全性性質：「データが失われない」「整合性が保たれる」等の時不変性質
  3. 活性性質：「要求は最終的に処理される」等の進歩性質
  4. 時相的制約：更新の順序、タイムアウト等の時間依存制約

目標：第7章のTLA+分散システム検証への準備

これらの演習を通じて、プログラミングの概念と数学的概念の対応関係を理解し、第3章以降の形式仕様記述技法への確実な基盤を築くことができます。次章では、これらの数学的概念を使って、曖昧性のない仕様を記述する具体的な技法を学んでいきます。