Extract spec

Extracting Provisional VDM-SL Specifications from Source Code

Extract structural and behavioral information from existing code and generate a PROVISIONAL VDM-SL specification as a starting point for dialogue with the user.

Critical principle: The spec extracted from code is NOT the true spec. It is a provisional scaffold for dialogue. The true spec exists in the user's head. Every extracted item must be tagged [PROVISIONAL] and framed as a question, not a statement.

<!-- 日本語 -->

既存のコードから構造情報と動作情報を抽出し、ユーザーとの対話の出発点となる 暫定的なVDM-SL仕様を生成する。

重要な原則: コードから抽出した仕様は「真の仕様」ではない。それはあくまで対話のための 暫定的な足がかりである。真の仕様はユーザーの頭の中に存在する。抽出した全ての項目には [PROVISIONAL]というタグをつけ、陳述ではなく質問として表現する。

Dialogue Flow

Step 1: Scope Identification

Ask the user which files or directories to analyze.

Questions to guide the scope:

1. Which files or directories should I analyze?
2. Are there entry points (main functions, API endpoints)?
3. Are there any main modules or key classes I should focus on?
4. Are there tests, documentation, or comments that explain the behavior?

<!-- 日本語 -->

ユーザーに、どのファイルまたはディレクトリを分析するかを質問する。

スコープを確定するための質問:

1. どのファイルまたはディレクトリを分析すべきか？
2. エントリーポイント（メイン関数、APIエンドポイント）はあるか？
3. 注目すべきメインモジュールやキークラスはあるか？
4. 動作を説明するテスト、ドキュメント、またはコメントはあるか？

Step 2: Structural Analysis

Read the code and extract candidates for:

Data Types

• Classes, interfaces, structs, dataclasses → VDM-SL record type candidates
• Enums → quote union candidates
• Optional/nullable types → optional type [T] candidates
• Union types → VDM-SL union type candidates
• Collections (arrays, lists, sets, maps) → sequence/set/map type candidates

Functions and Operations

• Function/method signatures → VDM-SL function/operation candidates
• Parameters and return types → type mappings
• State mutations (if any) → operation vs. function classification

Constraints and Validation Logic

• If-guards, assertions, validation functions → pre-condition candidates
• Return value patterns and state postconditions → post-condition candidates
• Invariants, decorators, schema validators → invariant candidates
• Test assertions → implicit specification evidence

<!-- 日本語 -->

コードを読み込み、以下の候補を抽出する：

データ型

• クラス、インターフェース、構造体、データクラス → VDM-SLレコード型の候補
• 列挙型 → クォート合併型の候補
• オプション型/nullable型 → オプション型 [T] の候補
• 合併型 → VDM-SL合併型の候補
• コレクション（配列、リスト、集合、辞書） → sequence/set/map型の候補

関数と操作

• 関数/メソッドのシグネチャ → VDM-SL関数/操作の候補
• パラメータと戻り値の型 → 型マッピング
• 状態変更（ある場合） → 操作 vs. 関数の分類

制約と検証ロジック

• if-ガード、assertions、検証関数 → 事前条件の候補
• 戻り値パターンと状態の事後条件 → 事後条件の候補
• 不変条件、デコレータ、スキーマバリデーター → 不変条件の候補
• テストのassertions → 暗黙的な仕様の証拠

Step 3: Provisional VDM-SL Generation

Convert extracted information to VDM-SL using the mapping rules in references/code-to-vdmsl-mapping.md.

Tagging Requirements: Every extracted line MUST be tagged with one of:

• [PROVISIONAL] — mechanically extracted from code, unconfirmed by user
• [QUESTION] — code behavior is questionable or ambiguous, user must confirm
• [IMPLICIT] — inferred from tests/comments/patterns, not explicitly in code
• [MISSING] — no corresponding code found, may need to be defined by user

Output format:

• File extension: .provisional.vdmsl
• Include source code reference for each extracted item (line numbers, function names)
• Comment each extraction with its provenance

Example:

-- [PROVISIONAL] Extracted from classes/user.ts lines 5-20
-- QUESTION: Is the email validation rule exactly as shown in the code?
types
  Email = seq1 of char
  inv email == email_valid(email)

<!-- 日本語 -->

references/code-to-vdmsl-mapping.md の変換ルールを使用して、抽出した情報を VDM-SLに変換する。

タグ付けの要件: 抽出した全ての行には、以下のいずれかをタグとして付ける必要がある：

• [PROVISIONAL] — コードから機械的に抽出、ユーザーにより未確認
• [QUESTION] — コードの動作が疑わしい、またはあいまい。ユーザーが確認する必要がある
• [IMPLICIT] — テスト/コメント/パターンから推論されたもの。コードに明示的にはない
• [MISSING] — 対応するコードが見つからない。ユーザーが定義する必要があるかもしれない

出力形式:

• ファイル拡張子: .provisional.vdmsl
• 抽出した各項目のコード参照（行番号、関数名）を含める
• 各抽出に出典コメントを付ける

例:

-- [PROVISIONAL] classes/user.ts lines 5-20から抽出
-- QUESTION: メール検証ルールはコードに示されているとおりですか？
types
  Email = seq1 of char
  inv email == email_valid(email)

Step 4: Uncertainty Identification

List all ambiguous or unclear points as "Questions for User".

Categorization:

• [UNCLEAR] — Code intent is unclear or ambiguous
• [AMBIGUOUS] — Multiple interpretations are possible
• [IMPLICIT] — Specification exists in tests or comments, not code
• [MISSING] — Feature appears in tests but not in implementation

Each question should present:

1. What the code appears to do
2. Why it's unclear or ambiguous
3. What the options are (if any)

Example:

[UNCLEAR] Type of `status` field in User class
Code:
  class User { status: string }
Question:
  - Is `status` constrained to specific values (e.g., "active", "inactive")?
  - Should we define an enumeration?
  - Or is any string value allowed?
Options:
  - Quote union: Status = <ACTIVE> | <INACTIVE> | <PENDING>
  - String with invariant: inv s == s in ["active", "inactive", "pending"]
  - Unconstrained: seq1 of char

<!-- 日本語 -->

あいまいまたは不明瞭なポイントを全て「ユーザーへの質問」としてリストアップする。

分類:

• [UNCLEAR] — コードの意図が不明瞭またはあいまい
• [AMBIGUOUS] — 複数の解釈が可能
• [IMPLICIT] — テストまたはコメントに仕様が存在。コードにはない
• [MISSING] — テストに表れているが実装されていない機能

各質問には以下を含める:

1. コードが何をしているように見えるか
2. なぜそれが不明瞭またはあいまいなのか
3. 何か選択肢があれば、その選択肢は何か

例:

[UNCLEAR] Userクラスの `status` フィールドの型
コード:
  class User { status: string }
質問:
  - `status` は特定の値（例："active"、"inactive"）に制限されているか？
  - 列挙型を定義すべきか？
  - それとも、任意の文字列値が許容されるのか？
オプション:
  - クォート合併型: Status = <ACTIVE> | <INACTIVE> | <PENDING>
  - 不変条件を持つ文字列: inv s == s in ["active", "inactive", "pending"]
  - 制約なし: seq1 of char

Step 5: Extraction Report

Produce a summary report covering:

1. What was extracted

   • Types found, operations found, pre/post/invariant candidates
   • Count of each category

2. What wasn't extracted

   • Missing constraints, unclear behavior, implicit specifications

3. Confidence levels

   • High: Clearly stated in code
   • Medium: Inferred from patterns, tests, or comments
   • Low: Ambiguous or conflicting evidence

4. Next steps

   • Explicit statement: "This is a provisional spec. Proceed to refine-spec for dialogue."
   • Recommend addressing unclear items first

<!-- 日本語 -->

以下を含む概要レポートを生成する:

1. 抽出したもの

   • 見つかった型、操作、事前/事後条件/不変条件の候補
   • 各カテゴリの数

2. 抽出されなかったもの

   • 欠落した制約、不明瞭な動作、暗黙的な仕様

3. 信頼水準

   • 高: コードに明確に記述されている
   • 中: パターン、テスト、またはコメントから推論された
   • 低: あいまいまたは矛盾する証拠

4. 次のステップ

   • 明示的な声明: 「これは暫定的な仕様です。refine-specに進んで対話してください。」
   • 不明瞭な項目を最初に扱うことを推奨

Important Notes

Framing as Questions, Not Statements

Never present extracted specifications as confirmed facts. Always frame them as questions.

WRONG: "The User type has a required email field of type string." RIGHT: "[PROVISIONAL] Does the User type require an email field of type string?"

WRONG: "The updateUser operation takes a user ID and returns a boolean indicating success." RIGHT: "[QUESTION] Does the updateUser operation take a user ID and return a boolean (true=success, false=fail)?"

<!-- 日本語 -->

質問として表現する、陳述ではなく

抽出した仕様を確認された事実として提示してはいけない。常に質問として表現する。

悪い例: 「Userタイプには、型stringの必須メールフィールドがある。」 良い例: 「[PROVISIONAL] Userタイプに、型stringのメールフィールドが必須か？」

悪い例: 「updateUser操作は、ユーザーIDを受け取り、成功を示すブール値を返す。」 良い例: 「[QUESTION] updateUser操作は、ユーザーIDを受け取り、ブール値（true=成功、false=失敗）を返すか？」

Bugs in Code Become Bugs in the Provisional Spec

If the code contains a logic bug, the extracted spec will reflect that bug. Inform the user:

"Note: The provisional spec reflects what the code currently does, not necessarily what it should do. If you notice discrepancies between the spec and intended behavior, those may indicate bugs in the code that should be fixed."

<!-- 日本語 -->

コードのバグは暫定仕様のバグになる

コードにロジックバグが含まれている場合、抽出した仕様もそのバグを反映する。 ユーザーに以下を伝える:

「注意: 暫定仕様は、コードが現在やっていることを反映しており、 それがすべきこととは限りません。仕様と意図された動作の間に 矛盾に気づいた場合、それはコードの中のバグを示している可能性があり、 修正すべきです。」

Always Proceed to Refine-Spec

After extraction is complete, strongly recommend proceeding to the refine-spec skill for dialogue with the user. The refine-spec skill is designed to:

• Clarify ambiguities by asking targeted questions
• Confirm implicit specifications
• Identify missing constraints
• Build consensus on the true specification

<!-- 日本語 -->

常にrefine-specに進む

抽出が完了したら、ユーザーとの対話のためにrefine-specスキルに進むことを 強く推奨する。refine-specスキルは以下のように設計されている:

• ターゲットとした質問をすることであいまいさを明確にする
• 暗黙的な仕様を確認する
• 欠落した制約を識別する
• 真の仕様に関するコンセンサスを構築する

Reference Documentation

For detailed code-to-VDM-SL mapping rules, see references/code-to-vdmsl-mapping.md.

For VDM-SL syntax and formal methods concepts, refer to the formal-methods-guide skill.

<!-- 日本語 -->

参照ドキュメント

詳細なコードからVDM-SLへのマッピングルールについては、 references/code-to-vdmsl-mapping.md を参照してください。

VDM-SLの文法と形式手法の概念については、formal-methods-guideスキルを 参照してください。