name: reconcile-code description: > Reconcile existing code with the confirmed VDM-SL specification. Compare spec vs code item-by-item, generate a diff report, produce code fixes prioritized by Finding category, and auto-generate tests. Triggered by: "reconcile code with spec", "fix code to match spec", 「仕様とコードを照合して」「コードを仕様に合わせて」「差分を出して」「コードを直して」 metadata: version: "1.3.0"
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:
- Show the specific code that's wrong (with line numbers)
- Explain how it differs from the spec
- Generate the fixed code (before/after diff)
- 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:
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:
- Explain what spec item is unimplemented
- Show where the code should have this logic
- Generate new code to implement the gap
- 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:
-
Valid input test — Operation succeeds without throwing
- Name:
test_<operationName>_with_valid_inputs_succeeds - Verify: No exception thrown, return value present
- Name:
-
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
- Name:
-
Boundary value tests — Test limits of pre-condition
- Name:
test_<operationName>_<conditionName>_boundary_<value> - Verify: Behavior at min/max allowed values
- Name:
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: 各前提条件について、以下をカバーするテストを生成:
- 有効入力テスト — 操作がスロウなしで成功
- 前提条件違反テスト — 各条件が個別のテストを作成
- 境界値テスト — 前提条件の制限をテスト
Post-condition Tests
EN: For each post-condition, generate tests:
-
Valid input verification — Return value matches post-condition
- Name:
test_<operationName>_returns_correct_<property> - Verify: Specific properties in return value match spec
- Name:
-
State change verification — State mutations match post-condition
- Name:
test_<operationName>_state_mutation_<stateName> - Verify: State changed as guaranteed by post-condition
- Name:
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: 各後提条件について:
- 有効入力検証 — 戻り値が後提条件と一致
- 状態変化検証 — 状態変異が後提条件と一致
Invariant Tests
EN: For each invariant, generate:
-
Valid construction test — Object created with valid state
- Name:
test_<className>_valid_construction_succeeds - Verify: Object created, invariant holds
- Name:
-
Invariant violation at construction — Invalid construction fails
- Name:
test_<className>_violates_<invariantName>_at_construction_fails - Verify: Construction throws appropriate error
- Name:
-
Invariant violation at mutation — Attempted mutation rejected
- Name:
test_<className>_mutation_violates_<invariantName>_rejected - Verify: Mutation prevented or error thrown
- Name:
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: 各不変式について:
- 有効な構築テスト — 有効な状態でオブジェクトが作成される
- 不変式違反テスト — 無効な構築が失敗
- 変異違反テスト — 試行された変異が拒否される
Finding-Specific Tests
EN: For each Bug or Spec Gap Finding:
-
Regression test — Tests that the bug fix works
- Reference the Finding ID
- Test the specific scenario that was failing
- Verify fix behavior
-
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 について:
- 回帰テスト — バグ修正が機能することをテスト
- 新しい動作テスト — 新たに実装されたフィーチャーをテスト
Test Framework Detection
Detect the test framework from:
- Package.json dependencies (jest, vitest, mocha, pytest, unittest, etc.)
- Existing test files in project (*.test.js, .spec.js, test_.py, *_test.py, etc.)
- tsconfig.json or pytest.ini configuration
- 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