スキルリファレンス

トリガーフレーズ:

ワークフロー:

1. エージェント情報の収集 — 名前、役割、入力、出力、関係性
2. 型定義の生成 — 自然言語をVDM-SL型に変換
3. 操作と契約の定義 — 質問を通じてpre/post/invを獲得
4. VDM-SL仕様の生成 — 全定義を含む完全なモジュール
5. レビューと反復 — ユーザー確認のため仕様を提示

組み込みテンプレート:

• 変換エージェント — ステートレスな入出力変換
• CRUDエージェント — 状態を持つ作成・読取・更新・削除
• パイプラインエージェント — 逐次的なデータ処理ステージ
• メディエーターエージェント — 複数サブエージェントの統合
• バリデーションエージェント — 入力検証とサニタイズ
• 設計文書テンプレート（v2.0.0） — Phase 2プロトコル・API設計文書
• ハイブリッド判定エージェント（v2.0.0） — スコアベースの複合判定

トリガーフレーズ:

ワークフロー:

1. VDM-SLファイルの探索 — ワークスペース内の.vdmslファイルを検索
2. 構文・型チェック — VDMJによるエラー報告
3. 証明責務の生成 — VDMJ -pフラグで実行
4. 解釈と説明 — 各POを平易な言語に翻訳
5. POの分類 — 緊急度別にランク付け（重大/標準/情報）
6. 次のステップを提案 — SMT検証への進行を提示

トリガーフレーズ:

ワークフロー:

1. POの受け付け — verify-specの出力または直接入力から
2. 型宣言の生成 — VDM-SL型をSMT-LIBソートに変換
3. 補助定義の生成 — 不変条件、pre/postをdefine-funとして定義
4. PO式の変換 — VDM-SLの論理式をSMT-LIBに変換
5. 否定してcheck-sat — assert(not PO)で反射的検証
6. Z3の実行 — 各.smt2ファイルにソルバーを実行
7. 結果の解釈 — unsat=証明済み, sat=反例あり, unknown=タイムアウト

トリガーフレーズ:

ワークフロー:

1. VDM-SLファイルの読み込み — 仕様をパース
2. 対象言語の確認 — TypeScript、Python、または両方
3. 型の変換 — VDM-SL型を対象言語の型に変換
4. 型定義の生成 — 不変条件付きのinterface/dataclass
5. 契約コードの生成 — pre/post/invのバリデーション関数
6. 操作スタブの生成 — 契約ラッパー付きの関数スキャフォールド
7. ファイル出力 — generated/ディレクトリに保存

トリガーフレーズ:

ワークフロー:

1. VDM-SL仕様と設計文書の読み込み — 不変式、契約、プロトコル規則をカタログ化
2. 型不変式テストの生成
3. 事前/事後条件テストの生成
4. 設計文書からプロトコルテストを生成: メッセージ型・ペイロード整合性と状態遷移（PROTOCOL.md）、APIシグネチャ（API-SIGNATURES.md）
5. 境界値テストの生成
6. テストファイルの出力 — Jest/Vitest互換

トリガーフレーズ:

ワークフロー:

1. 仕様の解析 — 永続化対象を特定：record型、quote型、state定義、不変条件、atomic操作
2. 対象DBMS（PostgreSQL/MySQL/SQLite）と命名規約の確認
3. 写像規則 R1〜R18 の適用：record→テーブル、map state→キー付きテーブル、quote型→ENUM/CHECK、不変条件→CHECK/UNIQUE/FK/トリガー、atomic→トランザクション境界
4. DEVIATIONS.md（retrenchment表）の生成 — 各乖離に具体的な補償手段（トリガー / アプリ層契約チェック / 契約テスト）を割り当て
5. TRACEABILITY.md の生成 — 全不変条件・操作契約を担保箇所に対応付け。担保箇所なしは許容しない
6. DDLの検証（SQLite/psql/Dockerでの実行確認）と網羅性チェック

トリガーフレーズ:

ワークフロー:

1. 仕様を読み込み、module 単位に分割
2. モジュールごとに複雑度シグナルを収集（verify-spec の PO レポートがあれば併用）
3. スコアリング規則で層を割り当て（型定義のみ→light、陰仕様あり→light 禁止のファストパス付き）
4. 提案テーブルをユーザーに提示し、行単位の上書きを受け付け
5. model-routing.json（仕様の隣）と MODEL-ROUTING.md を出力

トリガーフレーズ:

ワークフロー:

1. セッション設定 — エージェント名、開始点、対象言語、SMTの有無
2. Phase 1: 定義 — define-contractでVDM-SL生成
3. Phase 2: 検証 — verify-specで構文/型/POチェック
4. Phase 3: 証明（オプション） — smt-verifyでZ3証明
5. Phase 4: 生成 — generate-codeでTS/Pythonスキャフォールド
6. Phase 5: テスト — generate-testsで契約テストを生成・実行
7. セッションレポート — 全フェーズの包括的サマリー

トリガーフレーズ:

ワークフロー:

1. 概念の特定 — ユーザーの質問をリファレンス資料に照合
2. 説明の提供 — VDM-SLの例付きで平易な言語で解説
3. 文脈へのリンク — ユーザーの現在の仕様と関連付け

トリガーフレーズ:

ワークフロー:

1. MD文書の読み込みとパース — 構造、見出し、リスト、テーブルを識別
2. 要件の分類 — 各項目を型、制約、操作、ルールに分類
3. 曖昧性の検出 — 曖昧な数量詞、未定義の用語、欠落したエラーケース、境界条件
4. 対話的解消 — 優先度順に曖昧性を提示し、対話で解決
5. VDM-SLの生成 — [REQ-nnn]トレーサビリティ付きタグ付き仕様を生成
6. ギャップ分析 — 前方/後方/完全性チェック
7. パイプラインへの接続 — 次のステップとしてverify-specまたはrefine-specを推奨

トリガーフレーズ:

ワークフロー:

1. VDM-SL仕様の読み込み — 型、状態、操作、不変条件をカタログ化
2. 出力設定の確認 — 対象読者、言語、形式、詳細度
3. 各構造の翻訳 — 型→定義、pre→前提条件、post→保証
4. 文書の構造化 — 概要、用語集、データモデル、操作、ビジネスルール
5. 品質チェック — 完全性、忠実性、可読性、一貫性
6. 保存と提示 — Markdownとして出力、次のステップを提案