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のような高信頼が求められる領域で特に効果的