1. はじめに

近年、ChatGPTをはじめとする生成AIは「自然言語からコードを自動生成する」場面で急速に活用されています。しかし実務開発では、曖昧な要求仕様 → 各自解釈 → 統合時に不整合という問題が依然として多発します。
これを解決する武器が 形式的仕様記述言語（Formal Specification Language） の一つ、VDM++ です。

VDM++を「コードを書くための言語」ではなく「システム契約を記述するための言語」として導入すると、ChatGPTと組み合わせて次のような効果が期待できます。

曖昧さの除去：事前条件・事後条件を厳密に書くことで、AIへの指示が明確になる
自動生成の品質向上：ChatGPTに仕様を渡すと、正確なコードが高確率で生成される
大規模開発への適用：複数チーム／複数モジュールでの整合性を保証できる

2. VDM++の基礎とChatGPTとの相性

2.1 VDM++とは

プログラミング言語ではない
→ 実装詳細ではなく、「何を満たすべきか」を記述する。
契約ベースの仕様言語
- 事前条件（Precondition）
- 事後条件（Postcondition）
- 不変条件（Invariant）

2.2 ChatGPTとの相性

ChatGPTは「曖昧な自然言語仕様」には弱いが、**明確な契約（Pre/Post）**には非常に強い。
人間にとっても「この関数は何を満たせば正しいか？」が共有できるため、レビュー／監査でも有効。

3. 実務的な開発フローへの適用例

従来の開発フロー：

要求 → 仕様（曖昧な自然言語） → 設計 → コーディング

VDM++を導入したフロー：

要求 → 仕様（VDM++で契約定義） → 設計（Python/TSなど具体化） → ChatGPTでコード生成

4. 実務に近い具体例

4.1 API仕様の曖昧さ

例：動物判定API

入力：画像
出力：犬 or 猫

問題：空入力や豚の画像を渡された場合、チームによって挙動が異なる。

Aチーム：空入力はエラーを返す
Bチーム：空入力は「猫」と返す
Cチーム：豚は「Unknown」と返す

→ 結合時にシステム全体の挙動がバラバラになる。

4.2 VDM++による厳密仕様

types
  Image = seq of char;
  Label = <Dog> | <Cat>;
  Error = <InvalidInput>;

class AnimalAPI
operations
  Classify: Image ==> Label
  Classify(img) ==
    is not yet specified
  pre
    len img > 0 and IsDogOrCatCandidate(img)
  post
    RESULT = <Dog> or RESULT = <Cat>;

  ClassifyOrError: Image -> Label | Error
  ClassifyOrError(img) ==
    if len img = 0 or not IsDogOrCatCandidate(img)
    then <InvalidInput>
    else Classify(img);
end AnimalAPI

Classify：契約上「犬か猫のみ」
ClassifyOrError：それ以外は明示的に <InvalidInput>

→ これに従えば、各チームで挙動が揺れない。

5. ChatGPTへの利用方法

5.1 仕様をそのまま渡す

以下のVDM++仕様に従ってPythonで関数を書いてください。

5.2 ChatGPTの強み

Pre/Postを読んで境界条件テストまで生成可能
NumPyやpandas、FastAPIなど具体フレームワークと接続するコードを設計レイヤーの指示と組み合わせれば即実装可能

6. 実務に近いシナリオ

6.1 金融システムの例

入力：残高、出金額
出力：新しい残高
問題：残高不足時の扱い（エラー／0に丸める／借越許可）が曖昧になりやすい
VDM++では Pre で「出金額 <= 残高」を明記すれば、AIは安全なコードのみを生成する。

6.2 医療システムの例

入力：患者データ（バイタル値）
出力：異常検知アラート
問題：欠損データや外れ値の扱いが不統一だと致命的
VDM++で「欠損値がある場合はを返す」と定義すれば、全チームで統一。

7. 導入時の実務Tips

段階導入：最初から全機能ではなく、ユースケース1つに限定して試す
契約カプセル化：VDM++クラスを「仕様カプセル」とし、設計クラスとは分離
トレーサビリティ表：VDM要素ID ↔ 実装クラス ↔ テストを対応付け
CI/CD統合：VDM仕様 → テストケース自動生成 → GitHub Actionsで自動検証

8. 学習コストとChatGPTの補完

VDM++は集合・論理記号など数学的基礎が必要だが、理系学部レベルの数学知識で十分
学習コストは2〜3ヶ月で読めるレベルになる
曖昧な部分はChatGPTに「この仕様を日本語で説明して」と指示すれば補完可能

9. まとめ

仕様がなければ正しさの定義はできない
VDM++で契約を定義すれば、ChatGPTは高精度でコードを生成する
実務では「契約カプセル」として仕様と設計を分離すると、保守性と拡張性が高まる
金融・医療・AI APIのような高信頼が求められる領域で特に効果的