要求定義・仕様記述・設計・検証の手引き × 3つの理論で統一する成果物定義

Kuniwak さん（@orga_chem）が、要求定義・仕様記述・設計・検証を統一的に定義する資料を公開し、大きな反響を呼んでいます。

知人から辞書（悪い意味）との評価をうけた資料を公開しました。要求が何か、仕様が何か、設計が何か、検証が何かを明確に説明できない方向けの資料です。

https://x.com/orga_chem/status/2028973674876051777

126 いいね・22 RT・127 ブックマーク（10,847 表示）を集めたこのポストが指すのは、Speaker Deck で公開されたスライド資料です。「辞書（悪い意味）」と評されるほどの網羅性を持ちながら、Jackson（要求論）・Hoare（CSP）・Meyer（DbC）という3つの理論的基盤で全体を貫く一貫した構成が特徴です。

なぜこの資料が必要なのか

ソフトウェア開発の現場では、「要求」「仕様」「設計」の区別が曖昧なまま開発が進むことが珍しくありません。

• 「この機能の仕様は？」と聞かれて、要求（何を解決したいか）を答えてしまう
• 「設計書を書いて」と言われて、仕様（何をするか）を書いてしまう
• テストケースが何を検証しているのか、要求なのか仕様なのか不明確

この曖昧さが、手戻り・認識ズレ・テスト漏れの根本原因になっています。Kuniwak さんの資料は、これら4つの成果物を数学的な基盤から明確に定義することで、チーム内の共通言語を確立しようとするものです。

基礎概念: イベント・状態機械・トレース・並行合成

資料の全体を貫く基礎概念は4つあり、下から順に積み上がるレイヤー構造になっています。

レイヤー3: 並行合成     複数の状態機械を組み合わせる操作
    ↑ 状態機械を使う
レイヤー2: トレース     状態機械の上を走る「実行パス」
    ↑ 状態機械の上で定義される
レイヤー1: 状態機械     状態とイベントと遷移の構造
    ↑ イベントで構成される
レイヤー0: イベント     最小単位（ボタン押下、時間経過など）

上位の概念は下位の概念なしには定義できません。トレースは状態機械がなければ経路を辿れず、状態機械はイベントがなければ遷移が起きません。この順序で理解することが重要です。

レイヤー0: イベント

状態遷移の引き金となる最小単位です。UI 操作、時間経過、通信など、さまざまな形態があります。

ユーザーが「送信」ボタンを押す  → イベント
3秒経過する                    → イベント
サーバーからレスポンスが届く      → イベント

イベント単体では「何かが起きた」という事実だけです。これが意味を持つのは、次のレイヤーである状態機械の中に置かれたときです。

レイヤー1: 状態機械（State Machine）

状態機械は「今どういう状態にあるか」と「何が起きたら（=どのイベントが発生したら）次の状態に変わるか」を定義したモデルです。構成要素は3つだけです。

身近な例として自動販売機で考えます。

┌──────────┐  お金を入れる  ┌──────────┐  ボタンを押す  ┌──────────┐
│ 待機中   │ ────────────→ │ 金額表示 │ ────────────→ │ 商品排出 │
└──────────┘               └──────────┘               └──────────┘
     ↑                                                      │
     └──────────────── 商品を取る ───────────────────────────┘

ポイントは、今の状態とイベントの組み合わせで次の状態が一意に決まることです。「金額表示」でなければ「ボタンを押す」は効きません。曖昧さがありません。

ソフトウェアの例としてログインフォームを見ます。

┌──────────┐  入力する   ┌──────────┐  送信する   ┌──────────┐
│ 未入力   │ ─────────→ │ 入力済み │ ─────────→ │ 送信中   │
└──────────┘            └──────────┘            └──────────┘
                                                  │       │
                                           成功 ──┘       └── 失敗
                                             ↓                  ↓
                                       ┌──────────┐     ┌──────────┐
                                       │ 完了     │     │ エラー   │
                                       └──────────┘     └──────────┘

自然言語で書くと「入力してから送信すると送信中になって、成功したら完了画面、失敗したらエラー画面」ですが、状態機械にすると取りうる全ての状態と遷移が網羅的に定義されます。「送信中にもう一度送信ボタンを押したら？」→ 遷移が定義されていないので受け付けない。この明示性が仕様記述で重要になります。

レイヤー2: トレース

トレースは、状態機械の中を実際にたどった道順です。状態機械が「地図」だとすれば、トレースは「その地図の上を歩いた足跡」に相当します。初期状態から連続的に遷移可能なイベント列の1つを指します。

ログインフォームの状態機械の上で:

トレースA（正常系）:
  [未入力] ──入力する──→ [入力済み] ──送信する──→ [送信中] ──成功──→ [完了]

トレースB（エラー系）:
  [未入力] ──入力する──→ [入力済み] ──送信する──→ [送信中] ──失敗──→ [エラー]

同じ状態機械（レイヤー1）から複数のトレースが生まれます。状態機械が「ルール」なら、トレースはそのルールに従った「実際の試合展開」です。後述する要求定義は「どのトレースを避けるべきか」で定義され、検証は「トレースの標本を使った確認」として定義されます。

レイヤー3: 並行合成

並行合成は、複数の状態機械を組み合わせて、より大きな状態機械を作る操作です。

アプリ全体を1つの状態機械で書くと状態数が爆発して理解不能になるため、仕様記述では小さな状態機械に分解します。並行合成はその逆で、分解した状態機械を組み合わせて元のアプリ全体の振る舞いを再現する操作です。

たとえば「フォーム」と「バリデーション」という2つの状態機械を考えます。

「フォーム」状態機械              「バリデーション」状態機械
┌──────┐  入力  ┌──────┐        ┌──────┐  入力  ┌──────┐
│ 空   │ ─────→│ 入力 │        │ 未検証│ ─────→│ 検証中│
└──────┘       └──────┘        └──────┘       └──────┘
                                                │    │
                                          OK ──┘    └── NG
                                           ↓              ↓
                                      ┌──────┐     ┌──────┐
                                      │ 有効 │     │ 無効 │
                                      └──────┘     └──────┘

「同期イベント集合」とは、両方の状態機械が同時に反応するイベントの集合です。上の例では「入力」が同期イベントで、フォームとバリデーションが同時に状態遷移します。並行合成すると以下のようになります。

┌──────────────┐  入力   ┌──────────────┐
│ 空 × 未検証  │ ──────→│ 入力 × 検証中│
└──────────────┘        └──────────────┘
                          │          │
                    OK ──┘          └── NG
                     ↓                   ↓
               ┌──────────────┐   ┌──────────────┐
               │ 入力 × 有効  │   │ 入力 × 無効  │
               │（送信可能）   │   │（送信不可）   │
               └──────────────┘   └──────────────┘

個々の状態機械が正しくても、組み合わせたときに想定外の状態（デッドロック、競合状態）が起きることがあります。設計は「仕様の並行合成がトップレベル仕様を満たすように」コンポーネントを構成し、Meyer の DbC で契約を明示してこの問題を防ぎます。

4つのレイヤーと4つの成果物の対応

この基礎概念のレイヤー構造は、後述する4つの成果物と対応しています。

基礎概念               成果物              問い
─────────────────────────────────────────────────
イベント          →  要求定義        「どの悪いイベント列を避けるか」
状態機械          →  仕様記述        「状態機械に分解して定義する」
トレース          →  検証            「トレースの標本で正しさを確認する」
並行合成          →  設計            「合成結果が仕様を満たすか保証する」

これらの概念を基盤に、4つの成果物が定義されます。

4つの成果物の明確な定義

1. 要求定義: 「何を避けるべきか」を定める

要求定義は「どんな悪いトレース・悪いイベント集合を避けるべきか」を定めるものです。

ここでの重要な視点は、要求を「何をしたいか」ではなく「何を避けるべきか」で定義していることです。これは Michael Jackson の要求工学（Problem Frames）の考え方に基づいています。

Michael Jackson の Problem Frames

Michael Jackson（コンピュータ科学者）は、ソフトウェア問題を「問題フレーム」として構造化する手法を提唱しました。

• 問題領域（Problem Domain）: ソフトウェアが作用する現実世界
• 要求（Requirement）: 問題領域で達成すべき性質
• 仕様（Specification）: ソフトウェアと問題領域の境界での振る舞い

要求は「現実世界の問題」であり、仕様は「ソフトウェアの振る舞い」です。この区別が曖昧だと、「ユーザーが求めていないもの」を正確に作ってしまう事態が起きます。

「何を避けるべきか」で書く記述例

同じ要求を、従来の書き方と Jackson 式で比較します。

EC サイトのカート機能:

銀行の送金機能:

「二重送金防止」をトレースで具体的に書くと、どのイベント列を排除すべきかが明確になります。

悪いトレース（これが起きてはならない）:

  [送金画面表示]
    → [金額入力: 10,000円]
    → [送信ボタン押下]
    → [処理中表示]
    → [タイムアウト表示]      ← ユーザーには失敗に見える
    → [送信ボタン再押下]       ← もう一度押す
    → [処理中表示]
    → [完了表示]
    → 結果: 20,000円が引き落とされている  ← 二重送金！

従来の「二重送金を防止する」では、どういう操作の流れで二重送金が起きるのかが曖昧です。

なぜ「避けるべきこと」で書くのか

1. 網羅性が上がる — 「できること」を列挙すると書き忘れが起きます。「やってはいけないこと」は、境界条件や異常系に自然と目が向きます。

「何をしたいか」で書いた場合:
  ✓ ログインユーザーは購入できる
  ✓ 在庫がある商品を購入できる
  （ここで満足して終わりがち）

「何を避けるべきか」で書いた場合:
  ✗ 未ログインで購入できてはならない
  ✗ 在庫0で購入が完了してはならない
  ✗ 同時購入で在庫がマイナスになってはならない  ← これに気づく
  ✗ 決済失敗なのに在庫が減ってはならない        ← これにも気づく

2. テストとの対応が直接的 — 「避けるべきトレース」はそのままテストケースになります。

要求: 在庫0で購入が完了してはならない

→ テストケース:
  1. 商品Aの在庫を0に設定
  2. 商品Aをカートに追加
  3. 購入ボタンを押す
  4. 検証: 購入完了画面が表示されないこと

3. 並行処理の問題が見える — 「何をしたいか」では見えにくい並行実行の問題が、「悪いイベント集合」として明示されます。

悪いイベント集合（同時に起きてはならない）:

  ユーザーAが商品Xの最後の1個を購入 ← 同時に起きると
  ユーザーBが商品Xの最後の1個を購入 ← 在庫がマイナスに

→ この2つのイベントが同時に成功してはならない

2. 仕様記述: 「何をするか」を分解する

仕様は「機能要求を人間が理解しやすい小規模な状態機械に分解」したものです。

トップレベル仕様（巨大な状態機械）
  ↓ 分解
┌──────────┐  ┌──────────┐  ┌──────────┐
│ ログイン  │  │ フォーム  │  │ エラー   │
│ 状態機械  │  │ 状態機械  │  │ 表示     │
└──────────┘  └──────────┘  └──────────┘

各状態機械は、取りうる状態・イベント・遷移を明確に定義します。これが CSP（Communicating Sequential Processes）の考え方です。

Hoare の CSP

C.A.R. Hoare が提唱した CSP は、並行システムを数学的に記述する理論です。

• プロセス: イベントの集合と、それらのイベントに対する振る舞いの定義
• トレースモデル: プロセスが実行可能なイベント列の集合
• 安定障害モデル: トレースに加え、プロセスが「拒否」するイベント集合を記述

安定障害モデルが重要なのは、「何ができるか」だけでなく「何を拒否するか」（=デッドロックや不正状態）を形式的に表現できる点です。仕様記述において「この状態ではこのイベントを受け付けない」を明示することで、仕様の完全性が向上します。

3. 設計: 「どう実現するか」を決める

設計は「仕様の並行合成がトップレベル仕様を満たすようにコンポーネントを設計」することです。

設計時に記述すべき内容:

ここで登場するのが Meyer の Design by Contract（契約による設計）です。

Meyer の Design by Contract

Bertrand Meyer が提唱した DbC は、ソフトウェアコンポーネント間の「契約」を明示する設計手法です。

呼び出し側（クライアント）の義務:
  → 事前条件を満たしてからメソッドを呼ぶ

提供側（サプライヤー）の保証:
  → 事後条件を満たした状態で処理を返す

両者の合意:
  → 不変条件はオブジェクトの生存期間中つねに成立する

設計において「自由度を残しつつ、動作が約束の中で決まる」状態を作るのが契約の役割です。実装の詳細は決めないが、守るべきルールは明確にする。これが仕様と設計の境界です。

4. 検証: 「正しく作れたか」を確認する

テストケースは「仕様のトレース・イベント集合の標本」を用いた正当性確認です。

テストが「何を検証しているのか」が明確になることで、テストカバレッジの議論も具体的になります。「要求の何%を標本化できているか」「仕様のどのトレースが未検証か」という問いが可能になります。

3つの理論の統合

この資料の価値は、3つの理論を個別に紹介するのではなく、開発プロセスの各段階に対応づけて統合している点です。

  要求定義          仕様記述           設計            検証
┌──────────┐   ┌──────────┐   ┌──────────┐   ┌──────────┐
│ Jackson  │──→│ Hoare    │──→│ Meyer    │──→│ トレース │
│ Problem  │   │ CSP      │   │ DbC      │   │ の標本   │
│ Frames   │   │ 状態機械 │   │ 契約     │   │          │
│          │   │ 並行合成 │   │ 事前/事後│   │          │
│ 悪いトレ │   │          │   │ 不変条件 │   │          │
│ ースの定義│   │ 分解     │   │          │   │          │
└──────────┘   └──────────┘   └──────────┘   └──────────┘
     ↑              ↑              ↑              ↑
  「何を避ける」  「何をする」   「どう作る」  「正しいか」

この流れにより、「要求のトレースが仕様の状態機械に反映され、設計の契約で保証され、テストの標本で検証される」というトレーサビリティが確保されます。

Kuniwak さんの実践: 画面仕様書の静的検査器

Kuniwak さんはこの理論を実践に移しています。2025年に公開されたブログ記事「画面仕様書への静的検査器を実装したらたくさんの欠陥を発見できた話」では、機械可読な仕様書に対する静的検査器の実装が紹介されています。

実装概要

発見した欠陥

15% の画面から約 40 件の欠陥を検出しました。

• 画面遷移図と UI 要素表の不整合
• インタラクション可能な UI 要素の記載漏れ
• リストの並び順指示の欠落
• 動的画像の拡大縮小指示の曖昧さ
• 重複した ID
• TODO コメントの残存

これらは人間のレビューでは見落とされやすいが、形式的な仕様記述があれば機械的に検出できる欠陥です。「仕様を形式的に書く」ことの実用的な効果を示す好例です。

AI 時代における位置づけ

AI がコードを生成する時代に、この資料の重要性はむしろ高まっています。

• AI に「何を作るか」を正確に伝えるには、要求と仕様の区別が不可欠
• AI の生成物を検証するには、事前条件・事後条件が明確な設計が必要
• AI のテスト生成を指示するには、「どのトレースを標本化すべきか」が分からなければならない

「要求→仕様→設計→検証」の各段階で何を定義すべきかが曖昧なまま AI にコード生成を依頼すると、「要求を満たさない仕様に基づく正確なコード」が量産されるリスクがあります。

まとめ

• 要求定義は「どんな悪いトレースを避けるべきか」を定めるもので、Jackson の Problem Frames に基づく
• 仕様記述は機能要求を「小規模な状態機械に分解」したもので、Hoare の CSP（安定障害モデル）が理論的基盤
• 設計は「仕様の並行合成がトップレベル仕様を満たす」ようにコンポーネントを構成し、Meyer の DbC（契約による設計）で事前・事後条件を明示する
• 検証は「仕様のトレースの標本」であり、何を検証しているかが明確になることでカバレッジ議論が具体化する
• 3つの理論の統合により、要求→仕様→設計→検証のトレーサビリティが一貫して確保される
• Kuniwak さんは理論を実践に移し、Go 製の仕様静的検査器（23ルール）で 15% の画面から約 40 件の欠陥を自動検出している
• AI 時代においても「何を作るか」の定義力が開発品質を左右するため、この体系的な成果物定義の重要性は増している

参考

• Kuniwak さんのポスト
• 要求定義・仕様記述・設計・検証の手引き（Speaker Deck）
• 画面仕様書への静的検査器を実装したらたくさんの欠陥を発見できた話 — Kuniwak ブログ
• 自動テストに限界を感じた私がなぜ形式手法に魅了されたのか — Kuniwak ブログ
• Problem Frames — Michael Jackson
• Communicating Sequential Processes — C.A.R. Hoare（PDF）
• Design by Contract — Bertrand Meyer