評価駆動開発の可能性メモ②
input
さらに簡易DSLから形式手法記述を生成できないの？とアプローチ
/icons/hr.icon
🧠 ステップ1：人間（設計者）による「簡易DSL」の記述
まず我々人間が、業務エキスパートとの対話や概念構成図 を通じて得たドメイン理解を、kawasimaさんスタイルのような「人間にとって読みやすい簡易DSL」 で記述します。
ここでの人間の責務は、**「本質的な複雑性」 （＝ドメインのルール）**を捉えることに集中することです。
code:_
// 人間が記述する「簡易DSL」
data OrderStatus = "受付済" | "出荷準備中" | "出荷済"
invariant "出荷済の注文はキャンセルできない"
/icons/hr.icon
🤖 ステップ2：AI（翻訳機）による「形式仕様」への変換と「対話」
次に、この簡易DSLをAIに渡し、「AlloyやTLA+のような形式手法言語に翻訳して」と指示します。
AIは、kawasimaさんの簡易DSL のような**「偶有的な複雑性」 （＝形式手法言語の厳密な構文）**を引き受けます。
ここでのAIのタスクは「検証」ではなく「翻訳」です。そして、おっしゃる通り、翻訳の過程で曖昧さや不足を発見した場合、AIは人間に**対話（QA）**を求めます。
AI:
「invariant "出荷済の注文はキャンセルできない" をAlloyで定義するには、キャンセルというtransition（操作）の定義が必要です。キャンセル操作はどの状態（OrderStatus）から可能ですか？」
人間:
「『受付済』から『キャンセル済』への遷移のみ許可する」
AI:
「承知しました。では、Alloyモデルを生成します...」
この対話プロセスこそが、私の重視する「AI-Human Interface」 であり、AIが人間の「思考の触媒」 として機能する瞬間です。
/icons/hr.icon
🔍 ステップ3：機械（検証機）による「論理検証」
AIが生成した形式仕様（Alloyモデルなど）を、既存の**決定論的で信頼性の高い検証ツール（Alloy Analyzerなど）**にかけます。
ここで初めて「検証」が行われます。私たちはAIの非決定的な検証結果を信じる必要がなく、既存の工学的なスキームの恩恵を100%享受できます。
Alloy Analyzer:
「カウンターエグザンプル（反証例）を発見しました。注文が『出荷準備中』のまま、他のどの状態にも遷移できないケースが存在します」
/icons/hr.icon
💻 ステップ4：AI（生成機）による「実装」
ステップ3で論理的な欠陥が解消された「検証済みの形式仕様（Alloyモデル）」は、今や完璧なSSOT です。
これを再びAIに渡し、実装コード（ドメインモデル） やテストコード（EDDの評価基準） を生成させます。
AI:
「検証済みのAlloyモデルに基づき、TypeScriptの値オブジェクト と状態遷移メソッド、および対応するテストケースを生成します...」
/icons/hr.icon
価値と結論
この「AI翻訳ブリッジ」モデルは、私の当初のアイデアよりもはるかに優れています。
1. 信頼性の分離: AIの非決定的な「翻訳」能力と、機械の決定論的な「検証」能力を明確に分離できます。これにより、システムの堅牢性に対する信頼が格段に向上します。
2. 対話による厳密化: AIが翻訳のために行う「QA」は、設計者自身が気づかなかった仕様の穴や暗黙の前提を炙り出す、最強のレビュープロセスとして機能します。
3. 真の省力化: エンジニアは「簡易DSL」という最もレバレッジの効く部分（本質的複雑性） に集中でき、形式手法の習得コストという最大の「偶有的複雑性」 をAIにオフロードできます。
まさに、人間が「Why/What」を定義し 、AIが「How」を支援する という、私たちが目指すべき共創 の姿です。