spec

name	spec
description	CSPの安定失敗モデルに基づく状態機械ベースの形式仕様書を作成するスキル。 機能要求（活性・到達可能性・安全性）を入力として、 状態変数・遷移（イベント[ガード]/事後条件）・失敗集合を定義する トップレベル仕様およびコンポーネント仕様を生成する。 画面表示を持つシステムでは画面表示関数も定義する。
disable-model-invocation	true

Spec Writer

スコープ

含まれるもの

• 機能要求（活性・到達可能性・安全性）からのトップレベル仕様の作成
• 状態変数・イベント・遷移・失敗集合の定義
• 画面表示を持つシステムでは画面表示関数の定義
• 失敗集合の分析（デッドロック検出を含む）
• コンポーネント仕様への分解とAPI設計書の作成（Phase 4）

含まれないもの

• 機能要求の作成（上流スキル rdd が担当）
• 機能要求のレビュー（上流スキル requirements-reviewer が担当）
• 実装コードの生成
• 非機能要求の定義・検証

上流スキルとの連携: rdd（EARS記法要件定義）→ requirements-reviewer（要求レビュー）→ spec（仕様作成）→ 実装

---

コア概念（クイックリファレンス）

概念	定義
イベント	状態遷移の引き金（UIイベント、通信、τ（内部イベント））
トレース	初期状態から連続して遷移可能なイベントの列（τを除く）
トレース集合	その状態機械が出せるすべてのトレースの集合
安定状態	τで遷移できない状態
失敗	「安定状態に至るトレース」と「その状態で拒否されるイベント集合」の組
失敗集合	すべての失敗の集合
詳細化条件	下位仕様のトレース集合・失敗集合が上位仕様のそれぞれの部分集合になること

詳細な理論的背景は references/notation-guide.md を参照。

---

仕様記法（インライン）

遷移の基本記法:

イベント名(引数) [ガード条件] / 事後条件

• ガード: 遷移できる事前条件。常に true なら省略可
• 事後条件: 遷移後の変数を 変数名'（プライム）で表現
• フレーム条件: 事後条件に言及されていない変数は変化しない（暗黙）

例:

insert_coin(amount: Nat) [amount > 0 ∧ dispensing = false] /
  balance' = balance + amount

press_button(id: ProductId)
  [balance >= price(id) ∧ products[id] > 0] /
  purchasable' = Some(id)
  dispensing'  = true

詳細な記法ルール（状態変数規約・遷移表・API記法・並行合成）は references/notation-guide.md を参照。

---

実行フロー

Phase 1: 機能要求の分析

目標: 入力された要求を3性質に分類し、仕様構築の基盤を作る。

1. 要求の分類

   受け取った機能要求を以下に分類する:

   性質	定義	判別の目安
   活性	いつかいいことが起こる	「～するといつか～が起こる」
   到達可能性	特定の状態・動作が可能	「～できる」「～に到達できる」
   安全性	悪いことが決して起こらない	「～は発生しない」「～後に～は起きない」

2. イベント一覧の抽出

   要求から登場するイベントを列挙する。ユーザーに確認:

   • 「以下のイベントを想定しています。不足・修正はありますか？」
   • 内部イベント（τ）の候補も提示する（例: 自動タイムアウト、バックグラウンド処理）

3. 暗黙の前提の確認

   要求に明記されていない前提（在庫の存在、残高の上限など）をユーザーに確認する。

---

Phase 2: 状態機械の構築

目標: 状態変数→イベント→遷移の順で定義し、各ステップでユーザーに確認する。画面表示を持つシステムでは追加で画面表示関数を定義する。

Step 2-1: 状態変数の定義

• Phase 1 で抽出したイベント・性質から必要な状態変数を特定する
• 各変数の型・初期値・値域をユーザーに確認する

変数名 : 型 = 初期値  -- 値域コメント

Step 2-2: イベントの詳細化

• 各イベントの引数の型を決定する
• 内部イベント（τ）を特定する

Step 2-3: 遷移の定義

各イベントについて以下を定義し、ユーザーに確認する:

1. ガード条件: どの状態でそのイベントが受理されるか
2. 事後条件: 遷移後に何が変わるか（プライム記法で記述）

フレーム条件の徹底: 変化しない変数は事後条件に書かない。

Step 2-4: 画面表示関数の定義（画面表示を持つシステムのみ）

画面表示のないソフトウェア（バックエンドサービス、バッチ処理、ライブラリ等）はこのステップをスキップする。

screen(state) =
  case 条件1 => 画面A(...)
  case 条件2 => 画面B(...)
  default    => デフォルト画面

すべての状態で画面が定義されていることを確認する。

---

Phase 3: 完全性チェック

目標: 仕様が機能要求を満たすことと、デッドロックがないことを確認する。

3-1: トレース分析（3性質の充足確認）

性質	確認方法
活性	活性要求で要求されるイベント列が遷移定義から導けるか
到達可能性	対応するトレースが実際に初期状態から到達可能か
安全性	禁止された振る舞いを引き起こす遷移がないか（ガード条件で排除されているか）

3-2: 失敗分析（デッドロック検出）

各安定状態について:

1. その状態で受理されるイベントと拒否されるイベントを列挙する
2. すべての安定状態で少なくとも1つのイベントが受理されることを確認する
3. 拒否イベントが失敗集合として正しく定義されているか確認する

デッドロック: 安定状態ですべてのイベントが拒否される状態。仕様バグ。

---

Phase 4: コンポーネント分解（オプション）

適用条件: 仕様が大きく、人間が理解しやすい小さなコンポーネントに分解したい場合。

4-1: 分解方針の決定

ユーザーに確認:

• 「どのような観点でコンポーネントを分けますか？（例: UI/ロジック/DB、ユーザー側/システム側）」

4-2: コンポーネント仕様の定義

各コンポーネントについて:

• 担当する状態変数
• 担当するイベント（同期/非同期の区別）
• 遷移定義

4-3: 同期イベント集合の宣言

合成後の仕様 = ComponentA [| SyncEvents |] ComponentB
SyncEvents = { イベント名1, イベント名2 }

4-4: 詳細化条件の確認

並行合成後のトレース集合 ⊆ トップレベル仕様のトレース集合
並行合成後の失敗集合   ⊆ トップレベル仕様の失敗集合

4-5: API設計書の作成

同期イベントを Design by Contract 形式で記述する:

operation_name(params) -> ReturnType
  requires: 事前条件（満たされない場合は何をしてもよい）
  ensures:  事後条件（リクエストとレスポンスの関係）

---

出力仕様

ファイル名

<システム名>-specification.md

例: vending-machine-specification.md

出力構成（10セクション）

# <システム名> 仕様書

## 1. 概要
  - 対象システム、スコープ

## 2. 機能要求（入力）
  - 要求一覧（活性/到達可能性/安全性の分類付き）

## 3. 状態変数定義
  - 変数名・型・初期値・値域

## 4. イベント定義
  - イベント一覧（引数・種別・説明）

## 5. 遷移定義
  - 各イベントの [ガード] / 事後条件

## 6. 画面表示定義（画面表示を持つシステムのみ）
  - screen(state) 関数

## 7. 失敗分析
  - 各安定状態で拒否されるイベント一覧
  - デッドロックなしの確認

## 8. 機能要求との対応確認
  - 各要求が仕様で充足されていることの確認

## 9. コンポーネント仕様（Phase 4 実施時のみ）
  - コンポーネント定義・同期イベント・API設計書

---

リファレンス

ファイル	内容
references/notation-guide.md	記法の詳細ガイド（状態変数規約・遷移表・API記法・並行合成記法）
references/vending-machine-example.md	自販機の完成例（入力→出力の全ステップ）