第3章　仕様記述の基本

3.1 仕様とは何か：理想と現実の架け橋

仕様の本質的役割

「仕様」という言葉を聞いたとき、多くの人は技術文書や要求定義書を思い浮かべるでしょう。しかし、仕様の概念はもっと広く、深いものです。仕様は、理想的なシステムの振る舞いと、現実の実装の間の架け橋なのです。

日常生活のアナロジーで考えてみましょう。建築家が設計図を描くとき、その図面は「建物がどうあるべきか」を表現しています。材料の種類、寸法、配置、構造的な関係。これらの情報により、施工者は具体的な建物を作ることができます。同様に、ソフトウェアの仕様は「システムがどう振る舞うべきか」を表現し、開発者はそれに基づいて具体的なコードを書きます。

しかし、建築の設計図とソフトウェアの仕様には重要な違いがあります。建築の設計図は主に静的な構造を記述しますが、ソフトウェアの仕様は動的な振る舞いを記述しなければなりません。「ユーザーがボタンを押したらどうなるか」「データベースに接続できない場合はどうするか」「二人のユーザーが同時に同じリソースにアクセスしたらどうなるか」。これらの動的な側面が、ソフトウェア仕様の複雑さの源泉です。

仕様の階層性

実際のソフトウェアプロジェクトでは、仕様は階層的に構成されます。最上位のビジネス要求から、システム仕様、モジュール仕様、そして個々の関数の仕様まで、異なるレベルでの記述が必要です。

ビジネス要求レベル: 「顧客は商品を購入できる」 システム仕様レベル: 「ユーザー認証、在庫確認、決済処理、配送手配を経て購入が完了する」 モジュール仕様レベル: 「決済モジュールは信用情報を検証し、課金処理を実行する」 関数仕様レベル: 「validateCreditCard関数は16桁の数字列を受け取り、チェックサムを確認する」

この階層性は偶然ではありません。人間の認知能力の限界により、一度にすべての詳細を把握することは不可能です。適切な抽象化により、各レベルで管理可能な複雑さに分解することが必要なのです。

仕様の多面性

仕様には複数の側面があります：

機能的側面: システムが「何をするか」 非機能的側面: システムが「どのように動作するか」（性能、可用性、セキュリティ） 制約条件: システムが「してはいけないこと」 品質属性: システムの「望ましい性質」

従来のソフトウェア工学では、主に機能的側面に焦点が当てられてきました。しかし、現代のシステムでは非機能的側面がしばしば成功の鍵となります。Amazonのようなクラウドサービスでは、「99.99%の可用性」「100ミリ秒以下の応答時間」といった非機能要求が、機能要求と同じかそれ以上に重要です。

形式的手法は、これらすべての側面を統一的な枠組みで記述する能力を提供します。

仕様の進化性

ソフトウェアの仕様は静的なものではありません。要求の変化、技術の進歩、利用者の学習により、継続的に進化します。この進化性を考慮した仕様記述が重要です。

形式的仕様の利点の一つは、変更の影響範囲を明確に把握できることです。ある仕様要素を変更したとき、他のどの部分に影響するかを数学的に分析できます。これにより、安全な変更と危険な変更を区別し、適切な検証を行うことができます。

3.2 曖昧性との戦い：自然言語の限界

自然言語の構造的限界

人間のコミュニケーションにおいて、自然言語は驚くべき表現力と柔軟性を持ちます。しかし、この柔軟性こそが、精密なシステム記述において問題となります。自然言語には、避けることのできない構造的な曖昧性があるのです。

語彙的曖昧性: 同じ単語が複数の意味を持つ例：「銀行」（金融機関 vs 川の銀行）、「ログ」（記録 vs 丸太）

構文的曖昧性: 文の構造の解釈が複数ある例：「古い男性と女性の医師」（古い（男性と女性）の医師 vs 古い男性と（女性の医師））

意味的曖昧性: 文の意味の解釈が複数ある例：「顧客は商品を返品できる」（いつまで？どのような条件で？どのような状態で？）

実用的曖昧性: 文脈に依存する解釈例：「適切な時間内に」（システムによって「適切」の基準が異なる）

仕様書における曖昧性の実例

実際のソフトウェア仕様書から、曖昧性の具体例を見てみましょう：

例1: 「システムはユーザーの入力を検証する」

どのような入力を？（すべて？特定の種類？）
どのような検証を？（形式チェック？内容チェック？）
いつ検証するか？（入力時？送信時？）
検証に失敗したらどうするか？

例2: 「データベースへの接続が失敗した場合、適切にエラーを処理する」

何を「失敗」とするか？（タイムアウト？認証エラー？ネットワーク障害？）
「適切な処理」とは？（リトライ？代替手段？ユーザー通知？）
どのくらいの時間をかけて処理するか？

例3: 「システムは高い性能を提供する」

「高い」とはどの程度？（他システムとの比較？絶対的な基準？）
どの操作の性能？（応答時間？スループット？）
どのような条件下で？（通常時？ピーク時？）

曖昧性がもたらす実際の問題

これらの曖昧性は、単なる理論的な問題ではありません。実際のプロジェクトで深刻な問題を引き起こします。

開発チーム内での解釈の違い：同じ仕様書を読んでも、フロントエンド開発者、バックエンド開発者、テスト担当者が異なる理解をする。

顧客との認識齟齬：開発チームが正しいと考える実装が、顧客の期待と異なる。

テストケースの不一致：テスト担当者の解釈と実装者の解釈が異なり、テストが要求を正しく検証しない。

保守時の混乱：元の開発者が去った後、新しい開発者が仕様を異なって解釈し、意図しない変更を加える。

曖昧性の定量的分析

興味深いことに、仕様書の曖昧性は定量的に測定できます。語学学における曖昧性解析の技術を応用すると、文書内の曖昧な表現の密度を計算できます。

図3-1: 仕様記述の曖昧性階層と形式化による改善

研究によると、典型的なソフトウェア要求仕様書では：

1ページあたり平均15-20個の曖昧な表現が存在
重要な機能要求の約30%が複数の解釈を許す
非機能要求の約50%が定量的な基準を欠く

これらの数字は、自然言語による仕様記述の構造的な限界を示しています。

図3-2: 仕様記述の精密度レベルと認知負荷軽減効果

曖昧性解決の従来手法とその限界

ソフトウェア工学では、自然言語の曖昧性に対処するため様々な手法が開発されてきました：

構造化文書: テンプレートや決まった形式による記述

利点：一定の一貫性を保てる
限界：構造内での曖昧性は解決されない

用語集: プロジェクト固有の用語の定義

利点：語彙的曖昧性を部分的に解決
限界：用語の定義自体が曖昧な場合がある

プロトタイプ: 動作する簡易版による仕様の具体化

利点：視覚的・体験的な理解を促進
限界：例外的ケースや内部動作は不明

レビューミーティング: 関係者間での解釈の確認

利点：人間の知識と経験を活用
限界：参加者の理解レベルや関心の違い

これらの手法は有効ですが、根本的な問題を解決するものではありません。曖昧性の完全な排除には、より厳密なアプローチが必要です。

形式的記述への動機

この曖昧性の問題こそが、形式的仕様記述の最大の動機です。数学的記法を使うことで、解釈の余地のない厳密な記述が可能になります。

ただし、形式的記述にも限界があることを理解する必要があります：

すべての要求が形式化できるわけではない
形式化には時間とスキルが必要
関係者全員が形式記法を理解できるとは限らない

したがって、実際のプロジェクトでは、自然言語と形式的記法を適切に組み合わせることが重要です。クリティカルな部分は形式的に記述し、その他の部分は自然言語で記述するという段階的なアプローチが現実的です。

3.3 事前条件と事後条件：操作の契約

契約という概念の力

プログラムの関数や操作を「契約」として捉える考え方は、形式的仕様記述の基礎となる重要な概念です。この契約の概念は、日常生活の契約書から着想を得ています。

商取引の契約書を考えてみましょう。「売主は商品Aを提供する。買主は代金Bを支払う。商品は配送日Cまでに引き渡される。」この契約には、明確な構造があります：

前提条件：契約が有効になるための条件（商品が存在する、買主に支払い能力がある）
義務：各当事者が果たすべき行為
保証：契約履行後に保証される結果

プログラムの操作も、同じ構造で記述できます。

事前条件：操作の前提

事前条件（precondition）は、操作が正しく動作するために満たされるべき条件です。これは、操作の「約束の範囲」を明確にします。

例えば、配列から要素を取得する操作を考えてみましょう：

operation get_element(array, index)
precondition: 
  - array is not null
  - 0 ≤ index < length(array)

この事前条件は、「操作の呼び出し側の責任」を定義しています。これらの条件を満たさずに操作を呼び出した場合、操作の振る舞いは保証されません。

事前条件の設計には、重要な選択があります：

厳密な事前条件: 操作の実装を簡潔にできるが、呼び出し側の負担が大きい 寛容な事前条件: 呼び出し側が使いやすいが、操作の実装が複雑になる

この選択は、システム全体の設計思想に関わります。防御的プログラミングでは寛容な事前条件を好み、契約プログラミングでは厳密な事前条件を好む傾向があります。

事後条件：操作の保証

事後条件（postcondition）は、操作が完了した後に成り立つべき条件です。これは、操作の「提供価値」を明確にします。

先ほどの配列要素取得操作の続き：

operation get_element(array, index) → result
precondition: 
  - array is not null
  - 0 ≤ index < length(array)
postcondition:
  - result = array[index]
  - array is unchanged

事後条件は、「操作の実装側の責任」を定義しています。これらの条件を満たさない実装は、契約違反です。

事後条件の記述では、「変更されるもの」と「変更されないもの」の両方を明示することが重要です。上記の例では、戻り値が正しいことだけでなく、配列自体が変更されないことも保証しています。

フレーム問題：何が変更されないか

プログラムにおける「フレーム問題」は、「操作によって何が変更されないか」を明示的に記述する問題です。これは、人工知能の分野で初めて認識された問題ですが、ソフトウェア仕様にも深く関わります。

例えば、銀行口座から引き出しを行う操作：

operation withdraw(account, amount)
precondition:
  - account.balance ≥ amount
  - amount > 0
postcondition:
  - account.balance = old(account.balance) - amount
  - account.number is unchanged
  - account.owner is unchanged
  - all other accounts are unchanged

「all other accounts are unchanged」という条件は、この操作が他の口座に影響しないことを明示しています。このような「変更されない」保証は、システムの予測可能性にとって重要です。

例外的事後条件

実際のシステムでは、操作が正常に完了しない場合があります。ネットワーク障害、リソース不足、予期しない入力など、様々な例外的状況が発生します。

これらの状況も、事後条件として記述できます：

operation transfer_money(from_account, to_account, amount)
precondition:
  - from_account.balance ≥ amount
  - amount > 0
normal postcondition:
  - from_account.balance = old(from_account.balance) - amount
  - to_account.balance = old(to_account.balance) + amount
exceptional postcondition (network_failure):
  - all accounts unchanged
  - failure_log updated
exceptional postcondition (insufficient_funds):
  - all accounts unchanged
  - error_count incremented

例外的事後条件を明示することで、エラー処理の要求も形式的に記述できます。

契約の継承とオーバーライド

オブジェクト指向プログラミングにおいて、継承関係にあるクラス間での契約の関係は重要な設計原則となります。リスコフの置換原則は、この契約の観点から理解できます。

子クラスでメソッドをオーバーライドする場合：

事前条件は弱くできる（または同じ）
事後条件は強くできる（または同じ）

これにより、親クラスの契約を期待するコードが、子クラスのインスタンスでも正しく動作することが保証されます。

契約プログラミングの実践

契約という概念は、実際のプログラミングでも活用できます。Eiffel言語では契約がファーストクラス機能として提供され、Java、C#、Pythonなどでもライブラリとして利用できます。

@requires(lambda args: args.amount > 0)
@requires(lambda args: args.account.balance >= args.amount)
@ensures(lambda args, result: args.account.balance == old(args.account.balance) - args.amount)
def withdraw(account, amount):
    account.balance -= amount

このような契約の記述により、実行時に条件の違反を検出でき、デバッグやテストに役立ちます。

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

不変条件の本質的意味

不変条件（invariant）は、システムが常に満たすべき性質です。これは、システムの「基本的な約束」であり、どのような操作を行っても破られてはならない制約です。

物理世界のアナロジーで考えると、エネルギー保存の法則のようなものです。どのような物理的過程が起こっても、エネルギーの総量は保存されます。同様に、ソフトウェアシステムにも、どのような操作が行われても保持されるべき性質があります。

不変条件は、システムの「一貫性」を保証する概念です。データベースの整合性制約、オブジェクトの状態制約、システム全体のリソース制約など、様々なレベルで不変条件が存在します。

データ不変条件

最も基本的な不変条件は、データ構造レベルでの制約です。

配列の不変条件：

invariant: 0 ≤ length ≤ capacity
invariant: ∀i ∈ [0, length). elements[i] is valid

連結リストの不変条件：

invariant: head = null ⇒ size = 0
invariant: head ≠ null ⇒ reachable_nodes(head) = size
invariant: ∀node. node.next ≠ null ⇒ node ≠ node.next (no self-loops)

二分探索木の不変条件：

invariant: ∀node. 
  (node.left ≠ null ⇒ node.left.value < node.value) ∧
  (node.right ≠ null ⇒ node.value < node.right.value)

これらの不変条件は、データ構造の操作（挿入、削除、更新）によって破られてはなりません。

ビジネス不変条件

より高いレベルでは、ビジネスルールを反映した不変条件があります。

在庫管理システム：

invariant: ∀product. product.stock_count ≥ 0
invariant: ∀product. product.reserved_count ≤ product.stock_count
invariant: sum(all_orders.quantities) = sum(all_products.reserved_count)

銀行システム：

invariant: ∀account. account.balance ≥ account.minimum_balance
invariant: sum(all_accounts.balance) = total_deposits - total_withdrawals
invariant: ∀transaction. transaction.from_amount = transaction.to_amount

ユーザー管理システム：

invariant: ∀user. user.email ≠ null ∧ is_valid_email(user.email)
invariant: ∀user. count(users_with_email(user.email)) = 1
invariant: ∀session. session.user ≠ null ⇒ user.is_active

システム不変条件

システム全体のレベルでも、重要な不変条件があります。

リソース管理：

invariant: allocated_memory ≤ total_memory
invariant: active_connections ≤ max_connections
invariant: cpu_usage ≤ 100%

セキュリティ：

invariant: ∀operation. requires_authentication(operation) ⇒ current_user.is_authenticated
invariant: ∀data. data.classification = "secret" ⇒ current_user.clearance_level ≥ SECRET

一貫性：

invariant: ∀replica. replica.data = master.data (eventually)
invariant: ∀cache_entry. cache_entry.timestamp ≤ current_time

不変条件の階層性

複雑なシステムでは、不変条件も階層的に構成されます。低レベルの不変条件を基礎として、より高レベルの不変条件が成り立ちます。

レベル1（データ構造）: 配列の境界チェック
レベル2（オブジェクト）: 口座の残高非負
レベル3（ビジネス）: 総残高の保存
レベル4（システム）: 全体のセキュリティポリシー

この階層構造により、各レベルで適切な抽象化を行いながら、システム全体の一貫性を保証できます。

不変条件の検証

不変条件が実際に保たれているかを確認するには、すべての操作について検証する必要があります。

静的検証：コンパイル時や実行前に、すべての可能な実行パスで不変条件が保たれることを証明する。

動的検証：実行時に不変条件をチェックし、違反を検出する。

形式的検証：数学的証明により、不変条件の保持を厳密に証明する。

不変条件の設計原則

良い不変条件の設計には、いくつかの原則があります：

最小性：必要最小限の制約のみを含む 独立性：他の不変条件と重複しない 検証可能性：効率的にチェックできる 理解可能性：ドメインエキスパートが理解できる 安定性：システムの進化に対して安定している

不変条件違反の対処

不変条件の違反が検出された場合の対処戦略も重要です：

予防：違反を起こしうる操作を禁止する検出：違反を早期に発見する仕組み回復：違反状態から正常状態への復旧報告：違反の原因分析と改善

3.5 実例で学ぶ：スタックの完全仕様化

スタックの非形式的理解

スタック（stack）は、プログラミングにおいて最も基本的なデータ構造の一つです。「後入れ先出し」（LIFO: Last In, First Out）の原則に従って要素を管理します。日常生活では、本の積み重ねや皿の重ねなどがスタックの例です。

多くの人は、スタックの動作を直感的に理解しています。しかし、この直感的理解を形式的な仕様に変換することで、曖昧性を排除し、実装の正しさを保証できます。

スタックの基本操作

スタックには、通常以下の操作があります：

create(): 空のスタックを作成
push(item): アイテムをスタックの最上部に追加
pop(): スタックの最上部のアイテムを削除し、そのアイテムを返す
top(): スタックの最上部のアイテムを削除せずに返す
isEmpty(): スタックが空かどうかを判定
size(): スタック内のアイテム数を返す

これらの操作を形式的に仕様化してみましょう。

状態の形式的表現

まず、スタックの状態を数学的に表現します：

Stack[T] = ⟨items: Sequence[T], capacity: ℕ⟩

where:
  T: 要素の型
  items: 要素の順序付きシーケンス（items[0]が最上部）
  capacity: スタックの最大容量

不変条件：

invariant: |items| ≤ capacity
invariant: capacity > 0

create操作の仕様

operation create(cap: ℕ) → Stack[T]
precondition:
  cap > 0
postcondition:
  result.items = ⟨⟩  (空シーケンス)
  result.capacity = cap

この仕様は明確です：正の容量で呼び出されると、空のスタックが作成されます。

push操作の仕様

operation push(stack: Stack[T], item: T) → Stack[T]
precondition:
  |stack.items| < stack.capacity
postcondition:
  result.items = ⟨item⟩ ∘ stack.items  (itemを先頭に追加)
  result.capacity = stack.capacity
  |result.items| = |stack.items| + 1

ここで ∘ はシーケンスの連結を表します。事前条件により、満杯のスタックへのpushは定義されていません。

pop操作の仕様

operation pop(stack: Stack[T]) → (Stack[T], T)
precondition:
  |stack.items| > 0  (スタックが空でない)
postcondition:
  stack.items = ⟨top_item⟩ ∘ result.0.items
  result.1 = top_item
  result.0.capacity = stack.capacity
  |result.0.items| = |stack.items| - 1

この仕様では、操作の結果として新しいスタックと取り出されたアイテムの組を返します。

top操作の仕様

operation top(stack: Stack[T]) → T
precondition:
  |stack.items| > 0
postcondition:
  result = stack.items[0]
  stack is unchanged

top操作はスタックを変更しないため、フレーム条件として「stack is unchanged」を明示しています。

isEmpty操作の仕様

operation isEmpty(stack: Stack[T]) → Boolean
precondition:
  true  (常に呼び出し可能)
postcondition:
  result = (|stack.items| = 0)
  stack is unchanged

size操作の仕様

operation size(stack: Stack[T]) → ℕ
precondition:
  true
postcondition:
  result = |stack.items|
  stack is unchanged

操作間の関係

個々の操作の仕様だけでなく、操作間の関係も重要です：

push-pop関係：

∀s: Stack[T], x: T.
  |s.items| < s.capacity ⇒
  pop(push(s, x)) = (s, x)

push-top関係：

∀s: Stack[T], x: T.
  |s.items| < s.capacity ⇒
  top(push(s, x)) = x

isEmpty-size関係：

∀s: Stack[T].
  isEmpty(s) ⟺ (size(s) = 0)

エラー処理の仕様

実際のシステムでは、事前条件違反の場合のエラー処理も必要です：

operation pop_safe(stack: Stack[T]) → (Stack[T], Option[T])
precondition:
  true  (常に呼び出し可能)
postcondition:
  |stack.items| > 0 ⇒ 
    (result.0, result.1) = (pop(stack), Some(top(stack)))
  |stack.items| = 0 ⇒
    (result.0, result.1) = (stack, None)

性能特性の仕様

形式的仕様には、性能特性も含めることができます：

performance characteristics:
  push: O(1) time, O(1) space
  pop: O(1) time, O(1) space  
  top: O(1) time, O(1) space
  isEmpty: O(1) time, O(1) space
  size: O(1) time, O(1) space

並行アクセスの考慮

マルチスレッド環境では、並行アクセスに関する仕様も必要です：

concurrency specification:
  - 複数のスレッドからの同時read操作（top, isEmpty, size）は安全
  - write操作（push, pop）は相互排斥が必要
  - write操作中のread操作の結果は未定義

仕様の完全性検証

作成した仕様が完全かどうかを検証するためのチェックリスト：

操作網羅性: 必要なすべての操作が定義されているか
状態遷移網羅性: すべての有効な状態遷移が可能か
エラーケース網羅性: すべての異常ケースが処理されているか
不変条件保持: すべての操作が不変条件を保持するか
操作関係性: 操作間の期待される関係が成り立つか

このスタックの仕様化により、実装者は明確な指針を得られ、テスト担当者は網羅的なテストケースを作成でき、利用者は正確な使用方法を理解できます。

章末課題

基礎理解演習1：曖昧性の特定

以下の自然言語仕様の曖昧な点を特定し、それぞれについて可能な解釈を列挙してください：

「ユーザーはシステムにログインした後、ファイルをアップロードできる。アップロードされたファイルは適切にウイルススキャンされ、問題がなければ保存される。大きすぎるファイルや不正なファイルは拒否される。」

各文に含まれる曖昧な表現を特定
それぞれの表現について、少なくとも2つの異なる解釈を提示
その曖昧性が実装にどのような影響を与える可能性があるかを説明

基礎理解演習2：契約の記述

以下の関数について、事前条件と事後条件を形式的に記述してください：

def binary_search(sorted_array, target):
    """
    ソート済み配列から目標値を探索し、
    見つかればそのインデックスを、
    見つからなければ-1を返す
    """

記述すべき内容：

事前条件（配列の状態、引数の制約など）
正常時の事後条件（戻り値、配列の状態など）
異常時の事後条件（該当する場合）
フレーム条件（変更されない部分）

実践演習1：キューの仕様化

スタックの例に倣い、キュー（先入れ先出し）データ構造の完全な仕様を作成してください：

状態の形式的表現
基本操作（enqueue, dequeue, front, isEmpty, size）の仕様
データ不変条件
操作間の関係性
エラー処理の考慮

実践演習2：電子メールシステムの不変条件

簡単な電子メールシステムを考え、以下の要素に対する不変条件を定義してください：

システムの構成要素：

ユーザー（ID、メールアドレス、パスワード）
メールボックス（受信箱、送信箱、ゴミ箱）
メッセージ（送信者、受信者、件名、本文、タイムスタンプ）

要求される不変条件：

データ整合性に関する不変条件（最低3つ）
セキュリティに関する不変条件（最低2つ）
ビジネスルールに関する不変条件（最低2つ）

発展演習：仕様の検証

あなたが作成したキューの仕様について、以下の検証を行ってください：

一貫性検証: 異なる操作の組み合わせで矛盾が生じないか
完全性検証: 想定されるすべての利用パターンがカバーされているか
実装可能性検証: 仕様を満たす効率的な実装が可能か
テスト戦略: この仕様に基づいてどのようなテストケースが必要か

これらの演習を通じて、形式的仕様記述の実践的なスキルを身につけていただけます。次章では、これらの概念を具体的なツール（Alloy）で実装し、仕様の検証を自動化する方法を学んでいきます。

第3章 仕様記述の基本