Reconcile Code Skill

Overview / 概要

This skill reconciles existing code with a confirmed VDM-SL specification through systematic comparison, generates diff reports, produces prioritized code fixes, and auto-generates comprehensive tests.

このスキルは、確認済みのVDM-SL仕様との間で既存コードを体系的に比較し、差分レポートを生成し、優先度付きコード修正を生成し、包括的なテストを自動生成します。

---

Step 1: Item-by-Item Comparison

Type Definitions

EN: For each VDM-SL type definition in the confirmed spec, locate the corresponding code type (TypeScript interface/type, Python dataclass, etc.):

• Verify all field names match spec exactly
• Verify all field types match spec types (accounting for language-specific representations)
• Verify optional/required markers match (nullable, Optional[], etc.)
• Check for extra fields in code not in spec
• Check for missing fields in code that are in spec

JP: 確認済み仕様のVDM-SL型定義ごとに、対応するコード型（TypeScriptインターフェース/型、Pythonデータクラスなど）を見つけます:

• すべてのフィールド名が仕様と正確に一致することを確認
• すべてのフィールド型が仕様型と一致することを確認（言語固有の表現を考慮）
• オプション/必須マーカーが一致することを確認（nullable、Optional[]など）
• 仕様にない仕様にないコード内の余分なフィールドをチェック
• 仕様にあるがコードにない欠落フィールドをチェック

Status Codes:

• ✅ Match: All fields present, types correct, required/optional markers align
• ⚠️ Partial: Some fields missing/extra, or minor type representation differences that don't affect runtime
• ❌ Mismatch: Type definitions are incompatible, will cause runtime errors
• 🔍 Not Found: No corresponding type found in code

Pre-conditions

EN: For each VDM-SL pre-condition (guards in the function specification), find the corresponding code implementation:

• Look for guard clauses, early returns with error checks, parameter validation
• Verify the guard logic is equivalent to the pre-condition
• Check that appropriate errors/exceptions are thrown on violation
• Identify if the guard is implicit (e.g., type system enforces) or explicit (runtime check)

JP: VDM-SL仕様の各前提条件（関数仕様のガード）について、対応するコード実装を見つけます:

• ガード句、エラーチェック付きの早期リターン、パラメータ検証を探す
• ガードロジックが前提条件と等価であることを確認
• 違反時に適切なエラー/例外がスロウされることを確認
• ガードが暗黙的（型システムが強制）か明示的（実行時チェック）かを識別

Status Codes:

• ✅ Match: Guard logic matches spec, error handling present
• ⚠️ Partial: Guard exists but may be weaker than spec, or error handling incomplete
• ❌ Mismatch: Guard logic differs from spec or missing entirely
• 🔍 Not Found: No corresponding guard in code

Post-conditions

EN: For each VDM-SL post-condition (expected behavior after operation), verify the code implements it:

• Check return value structure and content against post-condition guarantees
• Verify state mutations match post-condition expectations
• Confirm side effects are correctly implemented
• Check that return values are validated before returning

JP: VDM-SL仕様の各後提条件（操作後の期待される動作）について、コードがそれを実装していることを確認します:

• 後提条件の保証に対して戻り値の構造と内容を確認
• 状態変異が後提条件の期待と一致することを確認
• 副作用が正しく実装されていることを確認
• 戻り値が戻る前に検証されることを確認

Status Codes:

• ✅ Match: Return values match post-condition, state changes correct
• ⚠️ Partial: Post-condition partially implemented, some guarantees missing
• ❌ Mismatch: Implementation doesn't match post-condition behavior
• 🔍 Not Found: No implementation found

Invariants

EN: For each VDM-SL class invariant, identify where validation must occur:

• Find invariant checks at object construction points
• Check all mutation points that could violate invariant
• Verify invariants are enforced consistently
• Identify if invariants are encoded in types or checked at runtime

JP: VDM-SLクラス不変式ごとに、検証が必要な場所を特定します:

• オブジェクト構築時の不変式チェックを見つける
• 不変式を違反する可能性のあるすべての変異ポイントをチェック
• 不変式が一貫して強制されることを確認
• 不変式が型にエンコードされているか実行時にチェックされるかを識別

Status Codes:

• ✅ Match: Invariants enforced at all critical points
• ⚠️ Partial: Invariants enforced at construction but not all mutation points
• ❌ Mismatch: Invariants violated or inconsistently enforced
• 🔍 Not Found: No invariant enforcement found

Reconciliation Table Output

Present results in a formatted table:

┌─────────────────────┬──────────┬─────────────────────┬─────────────┐
│ Spec Item           │ Status   │ Code Location       │ Note        │
├─────────────────────┼──────────┼─────────────────────┼─────────────┤
│ User (Type)         │ ✅ Match │ src/User.ts:10-25   │ -           │
│ createUser (Pre)    │ ❌ Mis   │ src/User.ts:30      │ Missing null│
│ createUser (Post)   │ ⚠️ Part  │ src/User.ts:30-40   │ Partial ID  │
│ UserInvariant       │ 🔍 Found │ -                   │ No check    │
└─────────────────────┴──────────┴─────────────────────┴─────────────┘

---

Step 2: Fix Generation (prioritized by Finding category)

Priority High: Bug Fixes

EN: Code behavior differs from confirmed spec, causing runtime failures or incorrect results:

• Code implements wrong logic
• Missing critical guards that could cause crashes
• State mutations don't match spec guarantees
• Error types are wrong or errors aren't thrown

For each Bug Finding:

1. Show the specific code that's wrong (with line numbers)
2. Explain how it differs from the spec
3. Generate the fixed code (before/after diff)
4. Include the Finding reference and confidence level

Example structure:

Bug Fix #1: createUser() pre-condition validation missing
Finding: BUG-001 [Confidence: High]
Spec requirement: User email must be non-empty string
Code issue: No email validation before DB insert
Location: src/User.ts:35-45

Before:
```typescript
function createUser(user: any) {
  return db.insert(user);
}
```

After:
```typescript
function createUser(user: User) {
  if (!user.email || user.email.trim() === '') {
    throw new ValidationError('Email is required and must be non-empty');
  }
  return db.insert(user);
}
```

JP: コード動作が確認済み仕様と異なり、実行時エラーまたは不正な結果を引き起こす:

• コードが間違ったロジックを実装
• クラッシュを引き起こす可能性のある重要なガード欠落
• 状態変異が仕様の保証と一致しない
• エラー型が間違っているか、エラーがスロウされていない

Priority Medium: Spec Gap Fills

EN: Spec defines behavior but code lacks implementation:

• Missing validation logic
• Missing runtime contract checks
• Missing helper methods referenced in spec
• Missing error handling for exceptional cases

For each Spec Gap Finding:

1. Explain what spec item is unimplemented
2. Show where the code should have this logic
3. Generate new code to implement the gap
4. Include runtime contract checks

JP: 仕様は動作を定義していますが、コードは実装を欠いています:

• 検証ロジックを欠落
• 実行時契約チェックを欠落
• 仕様で参照されているヘルパーメソッドを欠落
• 例外的なケースのエラー処理を欠落

Priority Low: Type Safety Improvements

EN: Strengthen types to prevent potential issues:

• Replace overly permissive types (any, object) with specific types
• Add missing null/undefined checks
• Add boundary value validation
• Improve type inference with better annotations

JP: 潜在的な問題を防ぐための型の強化:

• 過度に許容度の高い型（any、object）を特定の型に置き換える
• 欠落したnull/undefinedチェックを追加
• 境界値検証を追加
• より良い注釈で型推論を改善

Fix Metadata

Each fix must include:

finding_id: BUG-001 or SPEC-GAP-002 or TYPE-SAFE-003
spec_reference: "User :: createUser pre-condition"
affected_file: src/User.ts
line_range: 35-45
severity: High | Medium | Low
confidence: High | Medium | Low
before_code: |
  function createUser(user: any) { ... }
after_code: |
  function createUser(user: User) { ... }
explanation: "Added email validation guard missing from pre-condition"

---

Step 3: Test Auto-Generation

Pre-condition Tests

EN: For each pre-condition, generate tests covering:

1. Valid input test — Operation succeeds without throwing

   • Name: test_<operationName>_with_valid_inputs_succeeds
   • Verify: No exception thrown, return value present

2. Pre-condition violation tests — Each condition creates a separate test

   • Name: test_<operationName>_violates_<conditionName>_throws_<ErrorType>
   • Verify: Specific error type thrown with correct message
   • Vary: One condition violation per test

3. Boundary value tests — Test limits of pre-condition

   • Name: test_<operationName>_<conditionName>_boundary_<value>
   • Verify: Behavior at min/max allowed values

Example (Jest):

describe('User.createUser pre-conditions', () => {
  test('valid input succeeds', () => {
    const user = { email: 'test@example.com', name: 'Test' };
    expect(() => User.createUser(user)).not.toThrow();
  });

  test('empty email throws ValidationError', () => {
    const user = { email: '', name: 'Test' };
    expect(() => User.createUser(user))
      .toThrow(ValidationError);
    expect(() => User.createUser(user))
      .toThrow('Email is required');
  });

  test('null email throws ValidationError', () => {
    const user = { email: null, name: 'Test' };
    expect(() => User.createUser(user))
      .toThrow(ValidationError);
  });
});

JP: 各前提条件について、以下をカバーするテストを生成:

1. 有効入力テスト — 操作がスロウなしで成功
2. 前提条件違反テスト — 各条件が個別のテストを作成
3. 境界値テスト — 前提条件の制限をテスト

Post-condition Tests

EN: For each post-condition, generate tests:

1. Valid input verification — Return value matches post-condition

   • Name: test_<operationName>_returns_correct_<property>
   • Verify: Specific properties in return value match spec

2. State change verification — State mutations match post-condition

   • Name: test_<operationName>_state_mutation_<stateName>
   • Verify: State changed as guaranteed by post-condition

Example (Jest):

describe('User.createUser post-conditions', () => {
  test('returns user with assigned ID', () => {
    const user = { email: 'test@example.com', name: 'Test' };
    const result = User.createUser(user);
    expect(result).toHaveProperty('id');
    expect(typeof result.id).toBe('string');
  });

  test('persists user to database', () => {
    const user = { email: 'test@example.com', name: 'Test' };
    const result = User.createUser(user);
    const retrieved = User.findById(result.id);
    expect(retrieved).toEqual(result);
  });
});

JP: 各後提条件について:

1. 有効入力検証 — 戻り値が後提条件と一致
2. 状態変化検証 — 状態変異が後提条件と一致

Invariant Tests

EN: For each invariant, generate:

1. Valid construction test — Object created with valid state

   • Name: test_<className>_valid_construction_succeeds
   • Verify: Object created, invariant holds

2. Invariant violation at construction — Invalid construction fails

   • Name: test_<className>_violates_<invariantName>_at_construction_fails
   • Verify: Construction throws appropriate error

3. Invariant violation at mutation — Attempted mutation rejected

   • Name: test_<className>_mutation_violates_<invariantName>_rejected
   • Verify: Mutation prevented or error thrown

Example (Jest):

describe('User invariants', () => {
  test('valid user construction succeeds', () => {
    const user = new User('test@example.com', 'Test', 18);
    expect(user.email).toBe('test@example.com');
    expect(user.age).toBeGreaterThanOrEqual(0);
  });

  test('negative age at construction fails', () => {
    expect(() => new User('test@example.com', 'Test', -1))
      .toThrow('Age must be non-negative');
  });

  test('setting negative age rejected', () => {
    const user = new User('test@example.com', 'Test', 18);
    expect(() => { user.age = -1; })
      .toThrow('Age must be non-negative');
  });
});

JP: 各不変式について:

1. 有効な構築テスト — 有効な状態でオブジェクトが作成される
2. 不変式違反テスト — 無効な構築が失敗
3. 変異違反テスト — 試行された変異が拒否される

Finding-Specific Tests

EN: For each Bug or Spec Gap Finding:

1. Regression test — Tests that the bug fix works

   • Reference the Finding ID
   • Test the specific scenario that was failing
   • Verify fix behavior

2. New behavior test — Tests the newly implemented feature

   • Reference the Finding ID and Spec item
   • Test the new implementation

Example:

describe('Bug Fix: BUG-001 - Email validation missing', () => {
  test('regression: empty email now properly rejected', () => {
    const user = { email: '', name: 'Test' };
    expect(() => User.createUser(user))
      .toThrow(ValidationError);
  });

  test('regression: whitespace-only email rejected', () => {
    const user = { email: '   ', name: 'Test' };
    expect(() => User.createUser(user))
      .toThrow(ValidationError);
  });
});

describe('Spec Gap Fill: SPEC-GAP-001 - User password validation', () => {
  test('password must be at least 8 characters', () => {
    const user = { email: 'test@example.com', password: 'short' };
    expect(() => User.createUser(user))
      .toThrow(/at least 8 characters/);
  });
});

JP: 各Bug または Spec Gap Finding について:

1. 回帰テスト — バグ修正が機能することをテスト
2. 新しい動作テスト — 新たに実装されたフィーチャーをテスト

Test Framework Detection

Detect the test framework from:

1. Package.json dependencies (jest, vitest, mocha, pytest, unittest, etc.)
2. Existing test files in project (*.test.js, .spec.js, test_.py, *_test.py, etc.)
3. tsconfig.json or pytest.ini configuration
4. If detection fails, ask user or default to project convention

Generate tests using the detected framework's syntax and conventions.

Test Organization

• File location: Place tests in same directory structure as source, or in dedicated test/ directory
• File naming: Match project convention (*.test.js, .spec.js, test_.py, etc.)
• Test grouping: Use describe/test blocks, test classes, or test functions per framework
• Test data: Use fixtures/factories if they exist in project
• Additive only: Never delete or modify existing tests
• Integration: Import/reference production code same way existing tests do

---

Step 4: Reconciliation Report

Generate a comprehensive summary:

Report Structure

EN:

# Reconciliation Report: [Project Name]

## Executive Summary
- Total spec items analyzed: N
- Matched: N (X%)
- Partial matches: N (X%)
- Mismatches: N (X%)
- Not found: N (X%)

## Finding Summary
- Bug Fixes (High priority): N
- Spec Gap Fills (Medium priority): N
- Type Safety Improvements (Low priority): N

## Test Generation Summary
- Pre-condition tests generated: N
- Post-condition tests generated: N
- Invariant tests generated: N
- Finding-specific tests generated: N
- Total tests generated: N

## Files Modified
- src/File1.ts (N fixes)
- src/File2.ts (N fixes)
- test/File1.test.ts (new file, N tests)

## Detailed Findings
[List each finding with details]

## Remaining Manual Work
[Identify any items that require manual review]

JP:

# 照合レポート: [プロジェクト名]

## エグゼクティブサマリー
- 分析された仕様項目の合計: N
- 一致: N (X%)
- 部分一致: N (X%)
- 不一致: N (X%)
- 見つからない: N (X%)

## 調査結果の要約
- バグ修正（高優先度）: N
- 仕様ギャップ埋め（中優先度）: N
- 型安全性改善（低優先度）: N

## テスト生成の要約
- 生成された前提条件テスト: N
- 生成された後提条件テスト: N
- 生成された不変式テスト: N
- 生成された調査結果特定テスト: N
- 生成されたテスト合計: N

## 修正されたファイル
- src/File1.ts (N修正)
- src/File2.ts (N修正)
- test/File1.test.ts (新規ファイル、Nテスト)

## 詳細な調査結果
[各調査結果の詳細をリスト]

## 残りの手動作業
[手動レビューが必要な項目を特定]

Important Notes / 重要な注意事項

EN:

• Always show all fixes to user before applying them to code
• Never modify code without explicit user approval
• Generated tests are additive — preserve all existing tests
• If multiple test frameworks exist, ask user which to prioritize
• Confidence levels guide whether to auto-apply or require approval
• High confidence fixes may be auto-applied if user has enabled auto-fix mode
• Reference Finding IDs consistently throughout report and code

JP:

• コード修正前に常にユーザーにすべての修正を表示
• ユーザーの明示的な承認なしにコードを修正しない
• 生成されたテストは加算的 — 既存のテストをすべて保持
• 複数のテストフレームワークが存在する場合、ユーザーにどちらを優先するかを確認
• 信頼レベルは自動適用するか承認が必要かを指示
• 高信頼度修正は、ユーザーが自動修正モードを有効にした場合、自動適用される可能性がある
• レポートとコード全体を通じて一貫してFinding IDを参照

---

Usage Patterns / 使用パターン

Trigger Phrases

EN:

• "reconcile code with spec"
• "fix code to match spec"
• "generate diff report"
• "produce code fixes"
• "auto-generate tests for reconciliation"

JP:

• 「仕様とコードを照合して」
• 「コードを仕様に合わせて」
• 「差分レポートを出して」
• 「コード修正を生成して」
• 「照合テストを自動生成して」

Integration Points

This skill is designed to work with:

• formal-agent-contracts/plugin.json — loads confirmed spec findings
• VDM-SL specification documents — source of truth
• Project source code — target of reconciliation
• Test frameworks — Jest, Vitest, Mocha, Pytest, Unittest, etc.

---

Version History

v1.3.0 (Current)

• Full item-by-item comparison for types, pre/post-conditions, invariants
• Three-tier fix prioritization (Bug/Spec Gap/Type Safety)
• Comprehensive test auto-generation
• Bilingual EN/JP documentation