最近、AI によるソフトウェア開発が盛り上がっている。
その様子を眺めていると、古き良き時代の夢が、いよいよ実現するんじゃないかという気がしてくる。
CASEツールの夢だ。
昔、Enterprise Architect（製品名）のようなツールでクラス図を書いて、そこからDB定義やORMのコードを自動生成する、という世界があった。
クラスを追加すればテーブルが生まれる。属性を変更すればカラムが変更される。モデルを修正したら、マイグレーションファイルまで自動生成してくれる。
素晴らしいじゃないか。
もちろん、昔からそういうことを目指したツールは存在していたし、一部は実現していた。ただ、現実のソフトウェア開発を丸ごと任せられるかというと、そう簡単にはいかなかった。
しかし、今ならAIがいる。
モデルを定義して、あとはAIがコードを生成する。変更したら勝手に追従してくれる。
ようやく夢が叶うんじゃないか？
モデリングは大事なのだ
僕は長らく、「ドメインモデリングとDB設計はとても大事」派閥に所属していた。
いや、今でも所属している。
業務を理解して、登場する概念を整理して、それぞれの関係を定義する。これをきちんとやっておけば、ソフトウェアの構造も整理しやすくなる。
少なくとも、何となくコードを書き始めるよりはずっと良い。
だから、AIにソフトウェアを作ってもらうにしても、まずドメインモデルをきちんと作るべきだと思っている。
ところで。
「雨の日なら2割引」
これをクラス図でどう表現すればいいんだろう？
あるいは、
「親一人につき子供二人まで半額」
これは？
親と子供の関係はモデル化できる。料金も、割引も、天候だってモデル化できるだろう。
でも、それらを組み合わせた業務上の制約は、クラス図だけでは表現できない。
RDBMSならCHECK制約や外部キーなどで一部は表現できるけれど、こうした条件付きの業務ルールまでDBの制約で扱うのは難しい。
つまり、モデリングをいくら頑張っても、肝心の業務上の制約が書けないのだ。
ならば制約を書けばいいじゃない
AI全盛期となった今、制約論理プログラミングが再び注目されている。
AIが生成したコードは、それっぽく動く。しかし、正しいことを保証してくれるわけではない。
ならば、満たすべき制約を別途定義して、それを使って検証すればいい。
理屈はわかる。
だが、制約論理プログラミングは難しい。
例えば、Prolog の制約ライブラリ CLP(FD) で「親一人につき子供二人まで半額」を表すなら、こんな感じだ。これは、半額になる人数を最大化する簡略化した例である。
:- use_module(library(clpfd)).
discounted_children(Parents, Children, Discounted) :-
Discounted in 0..Children,
Discounted #=< Parents * 2,
labeling([max(Discounted)], [Discounted]).
% ?- discounted_children(2, 5, D).
% D = 4.
親が2人、子供が5人なら、半額になるのは4人。確かにそうなる。
……とはいえ、これはまだ単純な例である。年齢制限、別の割引との併用、適用期間なんてものが入ると、さらに考えることが増える。
ちなみに、制約を満たす値を探すのではなく、そもそもプログラムが制約を破らないことを数学的に証明する、という方法もある。Leanのような定理証明支援系だ。
同じ「親一人につき子供二人まで半額」で考えると、例えばこんな感じになる。
def discountedChildren (parents children : Nat) : Nat :=
min children (parents * 2)
-- 半額の子供が実際の子供の人数を超えない
theorem never_exceeds_children (p c : Nat) :
discountedChildren p c ≤ c := by
simp [discountedChildren]
-- 親一人につき最大二人まで
theorem never_exceeds_parent_limit (p c : Nat) :
discountedChildren p c ≤ p * 2 := by
simp [discountedChildren]
こちらは、たまたま親二人・子供五人の場合に正しいという話ではない。どんな自然数の組み合わせでも、半額対象の人数が上限を超えないことを証明しようとしている。
なお、著者はこのコードが読めない。AIに作ってもらったからだ。AIが実装したコードの正しさを証明するコードを、またAIに作ってもらう。そして読めない。
……僕は一体、何を検証しているんだろう。
もちろん、これで証明できるのはここに書いた関数の性質だけだ。別に生成された実装の正しさや、業務ルールそのものの妥当性まで証明できるわけではない。
ただでさえソフトウェア開発は複雑なのに、AIが生成したコードの妥当性を検証するために、現場のエンジニア全員に制約論理プログラミングを習得してもらうのか？
現場が死ぬんじゃないか？
そこで、僕は考えた。
ドメインモデルに加えて、Gherkinのような、散文に近い形式で業務上の制約を定義できればいいんじゃないか。
例えば、
- 雨の日なら、商品を2割引にする
- 親一人につき、子供二人まで半額にする
- 注文確定後は変更できない。ただし管理者による取消は可能
こういうルールを、人間にもAIにも理解できる形式で記述する。
そしてAIに実装させ、同時にその制約を満たしていることも検証してもらう。
ドメインモデルと業務制約。
この二つがあれば、かなり理想的な開発環境になるんじゃないか。
……いや、待てよ。
どんな構文がいいんだ？
自然言語に寄せすぎると曖昧になるし、厳密に記述しようとすると、結局プログラミング言語になってしまう。
あかん。わからへん。
Claude、お前……
そんなことをClaudeと相談していた。
すると、Claudeが言う。
「ええかもしれんが、お前は考えていないことがある」
なんすか？
「制約はな、ビジネスの世界では頻繁に変わるんや」
ほげえ。
そうなのだ。
例えば、雨の日の2割引キャンペーンが、翌月には土日限定になるかもしれない。さらに翌月には、会員限定になるかもしれない。
しかも、既存の予約には以前のルールを適用しなければならない、なんて話もあり得る。
一度決めた制約が、いつまでも変わらないわけではない。
制約をきちんと記述する仕組みを作ったとしても、その制約自体が変わり続ける。
それをどう管理し、どう実装へ反映し、どう検証するのか。
結局、業務ルールの変更という、昔からソフトウェア開発者を悩ませてきた問題に戻ってきてしまった。
なんて現実世界は難しいんだ。
AIのおかげで古き良きCASEツールの夢が叶うかもしれないと思ったのに、どうやらまだまだ遠そうである。
ところがどっこい
……というブログを書こうと思って、ChatGPTと雑談していた。
「モデリング頑張っても制約が書けんのよ」
するとChatGPTが言う。
「実は、UMLには制約を書く仕組みがあります」
えっ？
「OCL（Object Constraint Language）という言語がありまして、UMLのモデルに対する制約を記述できます」
なんすか、それ。
調べてみると、OCLというのは、UMLのモデルに対して条件や不変条件、操作の事前条件・事後条件などを記述するための言語らしい。
例えば、「注文確定後は変更できない。ただし管理者による取消は可能」というルールも、操作ごとの事前条件などとして表現できる。
しかも、1990年代から存在している。
マジかよ。
もちろん、OCLで制約を書けることと、その制約から実装や検証を自動生成できることは別の話だ。業務ルールが変わり続ける問題だって解決しない。
でも、少なくとも「UMLでは制約を書けない」という僕の思い込みは間違っていた。
ドメインモデルと制約を組み合わせるという発想自体、何十年も前からあったわけだ。
あるんかい！！
なんすか。
じゃあ、制約って表現できるじゃん。