| name | loopeng-extract |
| description | loop-engineering の 0 段(抽出ループ)。元仕様(RFC、標準、自然言語の要求、既存コード)から要件を 採番チェックリスト台帳へ網羅的に抜き出し、トレーサビリティ・マトリクスを立てる。 「要件を抽出して」「仕様から要件に落として」「抽出台帳」「トレーサビリティ」と言われたとき、 または loop-engineering ルーターから 0 段として委譲されたときに使用する。 後続の loopeng-formalize(EARS/TLA+)はこの台帳が完成(全 ID `[x]`・欠番なし)してからでないと進めない。 通常は loop-engineering ルーターの判断(2 問ゲート)を通ってから使う。
|
loopeng-extract (0 段: 元仕様 → 要件への網羅的抽出)
EARS を書く前に、元仕様から要件を漏れなく抜き出す工程を必ず置く。
外ループ以降は「与えられた要件」を厳密に検証するが、抽出そのものの網羅は守らない。
漏れは各層の内側ではなく、この入口に落ちる(実例は references/lessons.md)。
原則は 過剰抽出は安全、漏れは危険。
採り過ぎは後で「背景」に落とせるが、採り損ねた要件は下流のどの層にも現れず出口でしか露見しない。
迷ったら採る。
既存コードから要件を逆抽出するときの罠: 現状の挙動をそのまま「正解」として写し取らない。コードのバグごと仕様化すると、抽出仕様も TLA+ モデルも同じバグを共有し、TLC が緑でもバグは残る。台帳では「現状コードはこう動く」と「本来の仕様として正しいか(要人間確認)」を別列に分け、後者を必ずレビュー対象にする。
入口: 仕様を全件走査して要件候補を出し切る
仕様の構造単位(走査アンカー)を選ぶ。文書の型で変わる。
「規範語 grep」は数あるアンカーの一つで、RFC 形式にしか効かない。
- 規範語のある文書(RFC 等): RFC 2119 の11語を grep で全件。大文字のみが規範(RFC 8174、
-i なし)/否定形を最長一致で前置/word boundary。例 grep -nE '\b(MUST NOT|SHALL NOT|MUST|SHALL|SHOULD|MAY)\b' spec.txt。
- 日本語の仕様書/PRD/規程: 規範表現「〜しなければならない/してはならない/する必要がある/することができる/必須/任意/推奨」。法令調なら条・項・号が単位。
- 構造化仕様(OpenAPI/protobuf/JSON Schema/状態遷移表): 機械可読なので全要素を列挙。エンドポイント×メソッド、各フィールド制約、表の全セル。grep でなくパーサで。
- ユーザーストーリー/チケット/PRD 散文: 各受け入れ条件・各箇条書きを単位に。規範語が無いので各文を候補列挙し「要件か/背景か」分類(LLM ドラフト→人レビュー)。
- IaC(Terraform/Pulumi/SST/CloudFormation 等): IaC コード/モジュール仕様を元仕様に、遷移・順序・並行・失敗時不変条件(create/update/replace/destroy、依存グラフと apply 順序、並行 apply、ロールバック整合)を要件へ抽出する。静的な宣言・命名・タグは対象外。
抽出後に「この単位を1つ残らず拾ったか」を仕様の目次/章立てと突き合わせる。
採番チェックリスト方式(毎ループの必須ゲート)
STOP: この台帳を完成させるまで外ループ(loopeng-formalize)へ進むな。assets/extract-template.md を tasks/loopeng/<Name>.extract.md にコピーして埋めることから始める。loop-outer/loop-middle/loop-inner は PreToolUse hook(hooks/loopeng-extract-gate.sh)が台帳を検査し、台帳なし・[ ] 残り・S-NNN 欠番のいずれかで機械的にブロックする。頭の中抽出・後埋めは hook で弾かれる。
頭の中でやると漏れる。消し込み可能なワークシートに落とす。1ファイルで完結させる。
assets/extract-template.md を tasks/loopeng/<Name>.extract.md にコピーし、元仕様を「## 台帳」へ写す(原文保全、行番号/条項を引くため)。- 走査アンカーごとに1行立て、一意 ID を連番で振る(
S-001...)。grep 規範文・各フィールド・各受け入れ条件が1行=1 ID。
- 各行を チェックボックス付き Markdown にし、出典と原文抜粋を併記。
- 各 ID を EARS の1文へ変換して同じ行に書き、変換し終えたら
[x]。1 ID が複数 EARS に割れてよい。
- 未チェック残り = 抽出途中。全 ID が
[x]・連番に欠番なしで入口を閉じる。この ID(S-xxx)がトレーサビリティ表の「仕様条項」列になる。
## 抽出台帳(tasks/loopeng/<Name>.extract.md)
- [x] S-001 RFC§7.4.1 「endpoint MUST send a Close frame ...」
→ WHEN closing the connection the system SHALL send a Close frame. (event)
- [ ] S-002 RFC§5.2 「RSV1, RSV2, RSV3 MUST be 0 ...」 ← 未変換=漏れ予備軍
台帳を省いて頭の中で抽出する、既存 EARS から逆に後埋めする、は禁止。台帳が無い/未完なら設計検証は未着手。
口頭の要求だけで原文が無いときも、その要求文を tasks/loopeng/ に書き起こして起点にする。
工程: トレーサビリティ・マトリクス(漏れの本命対策)
各 ID を 「仕様条項ID → 要件(EARS R番号) → 形式手法(TLA+ INV / Lean P番号) → テスト」を1行で対応づける表にする。
漏れが「空欄」という見える形になる。
| 仕様条項 | 要件(EARS) | 形式手法 | テスト |
|-----------------|------------|----------|-----------------|
| RFC§7.4.1 close | R-xx | Lean P7 | test_close_code |
| RFC§5.2 RSV | (空欄!) | - | - | ← 抽出漏れが見える
- 軽量なら Markdown 表で十分。
- 「形式手法は埋まるのに要件列が空」= 証明済みなのに駆動する要件が無い(実装に結線されない)非対称も一目で出る。
全ループ共通の消し込み台帳
このマトリクス1枚を全ループ共通の台帳として使い回す(各ループで別台帳を増やさない)。
マトリクスの各列が各ループの消し込み対象。列が全行埋まったかで網羅を判定する。
- 外ループ(loopeng-formalize): 各 R番号が
Next disjunct / Inv / temporal のどれかに対応するか。「形式手法」列が空の EARS 行=外ループの漏れ。
- 内ループ(loopeng-gherkin の正シナリオ追加): TLC 反例由来は機械変換で消し込み不要(1反例=1 feature)。手作業は正常系の受け入れシナリオで、「テスト」列が空の event/state 系 EARS 正常系=内ループの漏れ。
- 中ループ(loopeng-modelcheck)は新規チェックリスト不要(YAGNI)。TLC の全到達状態探索と survivor 列挙が機械的に担う。
抽出の網羅を底上げする2手(任意だが効く)
出口: 独立基準で漏れを逆検出(最後の砦)
抽出の完全性は証明できないので、実装の振る舞いを抽出系と独立な基準でテストして漏れを逆算する。
- ファジング: 不正/境界入力で落ちる・誤受理する=unwanted 漏れ。ドメイン非依存の第一手。
- 差分テスト: 信頼できるリファレンス実装と出力差=どちらかの要件漏れ。
- 性質ベーステスト: 抽出した不変条件を生成入力で叩く。
- 既製の適合性スイート(あるドメインだけ): WebSocket→Autobahn 等。大半のドメインに既製品は無いので無いのが普通と構える。
やらないこと
- 「巨大だから別タスク」と自分でスコープを縮めない。 依存先の仕様(別 RFC・別標準)も調べて抽出対象に含める。大きいものは MECE に分割して順に積む。分割はスコープ除外ではない。完了条件は「指定範囲が全て
[x] か、物理的に止まるまで」で、自発的な区切りを完了と偽らない(過剰抽出は安全・漏れは危険の出口側)。
- 成果物の置き場・管理番号の扱いは
../_shared/stealth-artifacts.md に従う(台帳は tasks/loopeng/ 配下、git 管理外。S-xxx を本体へ漏らさない)。
次の工程
台帳が閉じたら(全 ID [x]・欠番なし)、loopeng-formalize スキルで各要件を EARS + 状態/ドメインモデルへ構造化し、TLA+ spec に落とす。
