集約をどこまで機械的に導けるか――形式手法をベースとしたドメインモデリング

AI に任せられる範囲と人が介入する範囲を分ける基準は、判断の不可逆性にあると考えています。 すぐに直せる実装の細部は AI に任せられますが、後戻りしにくい判断まで AI だけに任せることには若干の不安が残り、人が介入する余地はいまだにありそうです。 たとえば AI がコードを正しく書けても、できあがったシステムがビジネスに合っているとは限りません。 ビジネスの進め方や判断の基準と、システムに組み込んだルールがずれていれば、機能が動いても使ってもらえないでしょう。 そのずれを実装後に直そうとすると、ビジネスロジックやデータの持ち方まで見直すこともあります。 ビジネスのルールをどう実装するかも、できるだけ AI に任せたいところです。 ただ、AI が私たちの日頃のやり取りや暗黙の前提まで把握しているわけではありません。 伝えきれていない前提があれば、AI が考えたルールと実際のビジネスで守

[mkusaka]

Quintの不変条件とモデル検査を使い、注文・予算・予約の例から集約候補や整合性境界を導く手順を解説します。