verify-spec

仕様検証スキル (v2.0.0)

VDM-SL仕様ファイルの構文チェック、型チェック、証明責務（PO: Proof Obligation）生成を実行し、開発者にわかりやすく結果を報告するスキルです。v2.0.0ではプロトコル層の整合性検証が追加されています。

概要

VDM-SLで記述された形式仕様は、以下の複数のレベルで検証が必要です：

1. 構文検証：VDM-SL文法に従っているか
2. 型チェック：型参照、型不整合がないか
3. 不変式検証：不変式が一貫しているか
4. 契約検証：前提条件と後提条件の整合性
5. 設計文書の完全性検証（新v2.0.0）：PROTOCOL.md、API-SIGNATURES.mdの内容の完全性と矛盾確認
6. 証明責務生成：形式証明が必要な条件を生成

このスキルはVDMJツール（ISO VDM-SLの標準実装）を使用して、これらの検証を自動実行します。

ステップ1：検証ファイルの指定

目的：検証対象のVDM-SLファイルを特定

ユーザーに以下の情報を聞き出します：

• ファイルパス：検証するVDM-SLファイル（.vdmsl形式）
• モジュール名：検証対象のモジュール（例：HybridJudgeAgent）
• 検証範囲：全モジュール / 特定の関数のみ
• 既存の検証結果：過去に検証したことがあるか、前回のエラーは何か

質問例：

検証するVDM-SLファイルを教えてください：
形式：ファイルパスまたはファイル名
例：/path/to/agents/HybridJudgeAgent.vdmsl

ステップ2：構文検証

目的：VDM-SL文法に従っているか確認

VDMJツールの構文チェッカーを実行し、以下を検証：

• キーワード（module, exports, definitions等）の正確性
• 型定義の文法（Record ::, = ... |等）
• 関数定義の文法（pre/postキーワード）
• クォーテーション（<,>の対応）
• コメント（--）の形式

報告内容：

構文検証結果
=============
✓ ファイル: /path/to/agents/HybridJudgeAgent.vdmsl
✓ エンコーディング: UTF-8
✓ 行数: 245行

✓ 構文チェック: PASSED

詳細：
- module定義: ✓
- 型定義: ✓ (8個の型を検出)
- 関数定義: ✓ (5個の関数を検出)
- pre/post条件: ✓

エラー例：

❌ 構文エラー (行127, 列14):
  予期しないトークン: 'def' の代わりに 'definitions' が必要
  
  126: export all
  127: defs
       ^^^^
  128:   Score = nat1
  
修正：'defs' → 'definitions'

ステップ3：型チェック

目的：型の定義と参照の整合性を確認

VDMJツールの型チェッカーを実行し、以下を検証：

• 全ての型参照が定義されているか
• 型の構造が一貫しているか
• 関数のシグネチャが正しいか
• 不変式の型が正しいか

報告内容：

型チェック結果
==============
✓ ファイル: HybridJudgeAgent.vdmsl

✓ 型チェック: PASSED

検出された型：
  [1] Score = nat1
  [2] Threshold = nat1
  [3] Action = <AutoReply> | <OperatorAndLLM> | <OperatorOnly>
  [4] Ticket = ::
       - id: nat1
       - title: seq of char
       - content: seq of char
       - priority: nat0
       - complexity_score: Score

関数シグネチャ：
  [1] decide : Ticket -> Score -> Score -> Action
  [2] scoreAll : (seq of Score) -> seq of Score
  [3] explain_decision : (Score * Score * Score * Action) -> seq of char