AIと共に進化する開発手法： 形式手法と関数型プログラミングの可能性

Transcript

1. AIと共に進化する開発⼿法： 形式⼿法と関数型プログラミングの可能性 関数型まつり2025 2025年6⽉14⽇ 株式会社ログラス 執⾏役員CTO 伊藤博志（いとひろ @itohiro73） 1
2. #fp_matsuri 2 ゴールドマン・サックスのテクノロジー部に新卒入社後、同社の機関システム開発に 従事。その後、VP/Senior Engineerとしてプラットフォーム開発に携わり、同社 発のJavaのOSSであるEclipse Collectionsのコミッター兼プロジェクトリード やOpenJDKへのコントリビュートを行うなど、OSS戦略を牽引。 スタートアップ2社を経て、READYFORに入社し執行役員VPoEに就任。 同社のエンジニア組織の10名から30名規模への成長、決済基盤の刷新や、技術的 負債の返済、新規プロダクト開発を牽引。 2022年10月に株式会社ログラスの開発部へエンジニアとして入社。 エンジニアリングマネージャー、事業執行役員VPoEを経て、現職。 株式会社ログラス 執行役員 CTO 伊藤 博志 （いとひろ @itohiro73） Hiroshi Ito ⾃⼰紹介
3. #fp_matsuri 1. AIエージェントを⽤いた開発の特徴 2. 形式⼿法を⽤いた仕様モデリングと検証 3. 代数的データ型(ADT)と関数型ドメインモデリングの利点の活⽤ 4. プロパティベーステストによる性質の検証 5. シフトレフトアプローチのAI開発適⽤ 本⽇のアジェンダ 3
4. #fp_matsuri みなさん、開発でAIコーディングエージェント （Cursor、Cline、Devin、Claude Code等々）使っていますか？ AIエージェントを⽤いた開発の特徴 4 🤚 会場アンケート
5. #fp_matsuri AIエージェントによる開発では、従来の⼈間中⼼の開発プロセスとは異なる特性が 顕著に現れる • 物量の多さ: とにかく⼀度に実装する物量が多い。適切なガードレールがないと 必要ないものもどんどん追加する • コンテキストの理解の限界: プロジェクトの複雑な依存関係や暗黙的な要件を完 全に把握するの困難 • 品質保証の新たな課題: よしな⼒は⾼いので⼀定の品質のものは出てくる。しか し、AIエージェントによる開発‧改修が数年単位で積み重なった先にどうなる か、それはまだ誰も⾒ぬ世界 AIエージェントを⽤いた開発の特徴 5
6. 形式⼿法を⽤いた仕様モデリングと検証 6
7. #fp_matsuri 形式⼿法の基本概念 形式⼿法（Formal Methods）とは、数学的厳密さを基にシステムの仕様を厳密に記述し、その正し さを論理的推論をもちいて検証する⼿法の総称。 形式⼿法はソフトウェアがある性質を満たしていることを論理的に検証するため、⼀定の不具合が 存在しないことを保証できる。そのような点で、完全な網羅性を持たない従来のテストの問題点を 解決することができる。 ⼀⽅、形式⼿法をソフトウェアの開発プロセスに組み込むことは⾮常に運⽤コストが⾼いのがネッ クでもあった。 昨今のAIコーディングエージェントの勃興は、形式⼿法の活⽤シーンを増やし、かつコストさえも 低減してくれる可能性がある 形式⼿法とは何か 7
8. #fp_matsuri なぜ形式⼿法が重要なのか（これは仮説） AIコーディングエージェントとの協働において、形式⼿法が有⽤なのではないかと考える理由： • 曖昧性の排除：⾃然⾔語の曖昧さを形式⼿法が排除し、AIが進むべき道筋を明確化してくれる • 検証可能性：数学的記法により⾃動検証が可能 • 完全性の保証：すべての状態とケースを網羅的に記述 • コミュニケーション⼿段：⼈間とAIの共通⾔語 そして何よりも、AIコーディングエージェント⾃体が形式化を⼿伝ってくれる！ 形式⼿法とは何か 8
9. #fp_matsuri Alloyとは Alloyは構造的モデリングに特化した形式仕様⾔語です。Daniel Jackson⽒（MIT）により開発さ れ、「リレーショナルロジック」に基づいてシステムの静的な構造と制約を記述します。 Alloyの主な特徴： • 宣⾔的記述：「何をするか」ではなく「何であるべきか」を記述 • リレーション中⼼：オブジェクト間の関係を中⼼にモデリング • ⾃動的な反例⽣成：制約に違反する具体例を⾃動⽣成 • ⼩さなスコープでの網羅検証：有限範囲内で全パターンを検査 形式⼿法の例（Alloy） 9
10. #fp_matsuri TLA+とは TLA+（Temporal Logic of Actions）は、動的なシステムの振る舞いを記述するための形式仕様⾔語 です。Leslie Lamport（Microsoft Research）により開発され、並⾏システムや分散システムの時間 的特性を記述できます。 TLA+の主な特徴： • 時相論理：システムの時間的変化を数学的に記述 • アクション指向：状態変化を「アクション」として定義 • 並⾏性の明⽰的サポート：複数プロセスの相互作⽤を記述 • 活性‧安全性の検証：「悪いことは起こらない」「良いことはいずれ起こる」を証明 形式⼿法の例（TLA+） 10
11. ⾃然⾔語仕様から形式⼿法への 変換プロセス例 11
12. #fp_matsuri 書店システムの隠れた複雑性:⼀⾒シンプルな「本を注⽂する」機能 【基本要件】 ✓ 本の在庫を管理する ✓ 顧客からの注⽂を受け付ける ✓ 在庫から商品を引き当てる ✓ 注⽂を確定して配送⼿配する 要件実装事例: 書店システム 12
13. #fp_matsuri 書店システムの隠れた複雑性:⼀⾒シンプルな「本を注⽂する」機能 【基本要件】 ✓ 本の在庫を管理する ✓ 顧客からの注⽂を受け付ける ✓ 在庫から商品を引き当てる ✓ 注⽂を確定して配送⼿配する 要件実装事例: 書店システム 13 【隠れた複雑性‧曖昧性】 ⚠ 同時に100件の注⽂が来た時の在庫競合 ⚠ 予約注⽂と通常注⽂の優先順位 ⚠ 在庫切れ時の⾃動再発注 ⚠ 返品‧キャンセル時の在庫復元 ⚠ 複数倉庫間の在庫移動
14. #fp_matsuri 例えばAIが以下のようなコードを⽣成したら？ 要件実装事例: 書店システム 14 // AIが生成した危険なコード fun processOrder(bookId: String, quantity: Int, customerId: String): Boolean { val book = bookRepository.findById(bookId) if (book != null && book.stock >= quantity) { book.stock -= quantity // 🚨 同時注文時の競合状態 orderRepository.save(Order(customerId, bookId, quantity)) return true } return false }
15. #fp_matsuri 例えばAIが以下のようなコードを⽣成したら？ 要件実装事例: 書店システム 15 // AIが生成した危険なコード fun processOrder(bookId: String, quantity: Int, customerId: String): Boolean { val book = bookRepository.findById(bookId) if (book != null && book.stock >= quantity) { book.stock -= quantity // 🚨 同時注文時の競合状態 orderRepository.save(Order(customerId, bookId, quantity)) return true } return false } 何が問題？ シナリオ: 在庫1冊の本に対して2件の同時注⽂ 1. 注⽂A: book.stock >= 1 ✅ → book.stock = 0 2. 注⽂B: book.stock >= 1 ✅ → book.stock = -1 🚨 結果: 在庫がマイナスになり、存在しない商品を販売
16. #fp_matsuri どうすればよいか？ => AIエージェントが⼒を発揮するために必要なもの 1. 明確な枠組み（制約）の提供 ❌ 「在庫管理システムを作って」 ✅ 「在庫 ≥ 予約数」「同時更新は排他制御」など明確な制約 2. コンテキストの最⼩化 ❌ システム全体を⼀度に理解 ✅ 「在庫管理」「注⽂処理」「⽀払い」を独⽴したコンテキストに分離 形式⼿法 + 関数型プログラミング = 解決の鍵 形式⼿法: 数学的に厳密な仕様記述 関数型プログラミング: 型システムによる制約の実装 要件実装事例: 書店システム 16
17. #fp_matsuri 形式⼿法の活⽤ ⾃然⾔語による仕様書: 「在庫がある本のみ注⽂可能」→ 曖昧：在庫1冊に2件の同時注⽂は？ 形式仕様: 要件実装事例: 書店システム 17 fact NoOverbooking { all b: Book | { let totalOrdered = sum o: Order | (o.book = b and o.status != Cancelled) => o.quantity else 0 | let currentStock = sum inv: Inventory | (inv.book = b) => inv.stock else 0 | totalOrdered <= currentStock // 数学的に厳密 } }
18. #fp_matsuri 形式⼿法の活⽤ ⾃然⾔語による仕様書: 「在庫がある本のみ注⽂可能」→ 曖昧：在庫1冊に2件の同時注⽂は？ 形式仕様: 要件実装事例: 書店システム 18 fact NoOverbooking { all b: Book | { let totalOrdered = sum o: Order | (o.book = b and o.status != Cancelled) => o.quantity else 0 | let currentStock = sum inv: Inventory | (inv.book = b) => inv.stock else 0 | totalOrdered <= currentStock // 数学的に厳密 } } 利点 曖昧性の排除: ⾃然⾔語の「解釈の余地」をなくす 機械的検証: コンピュータが仕様の⽭盾を⾃動発⾒ AIへの明確な指⽰: 制約を型システムに直接反映可能
19. #fp_matsuri 形式⼿法の基本⽂法（Alloy） 19 Alloyの基本構⽂要素 1. Signature（sig） - エンティティの定義 sig Book { // Bookエンティティ isbn: ISBN, // isbnフィールド（ISBN型） title: String, // titleフィールド（String型） price: Money // priceフィールド（Money型） } sig Customer { name: String, email: String } // 関係の定義 sig Order { customer: one Customer, // 1つのCustomerに関連 books: set Book, // 複数のBookと関連 total: one Money }
20. #fp_matsuri 形式⼿法の基本⽂法（Alloy） 20 Alloyの基本構⽂要素 2. Multiplicity（多重度） - 関係の数を制約 customer: one Customer // 必ず1つ books: set Book // 0個以上（空集合も可） books: some Book // 1個以上 manager: lone Employee // 0個または1個
21. #fp_matsuri 形式⼿法の基本⽂法（Alloy） 21 Alloyの基本構⽂要素 3. Constraint（制約） - ビジネスルールの定義 alloysig Inventory { book: Book, stock: Int } { stock >= 0 // Signature内制約：在庫は非負 } fact GlobalConstraint { // グローバル制約 all i: Inventory | i.stock <= 1000 // すべての在庫は1000以下 }
22. #fp_matsuri 形式⼿法の基本⽂法（Alloy） 22 Alloy量詞と論理演算 量詞（Quantifiers）- 条件の範囲を指定 // all: すべての要素について all o: Order | o.total.amount > 0 // すべての注文の金額は正数 // some: 少なくとも1つの要素について some o: Order | o.status = Shipped // 少なくとも1つの注文が発送済み // no: 存在しない no o: Order | o.total.amount < 0 // 負の金額の注文は存在しない // lone: 最大1つ lone o: Order | o.status = Cancelled // キャンセル注文は最大1つ // one: 必ず1つ one o: Order | o.customer = Alice // Aliceの注文は必ず1つ
23. #fp_matsuri 形式⼿法の基本⽂法（Alloy） 23 Alloy量詞と論理演算 論理演算と集合演算 // 論理演算 and, or, not, implies, iff // 集合演算 in // 包含関係：A in B（AはBに含まれる） + // 和集合：A + B & // 積集合：A & B - // 差集合：A - B ~ // 転置：~r（関係rの逆） ^ // 推移閉包：^manager（管理者の推移的関係）
24. #fp_matsuri Alloyによる構造的モデリング 24 書店システムの基本構造を定義 sig Book { isbn: ISBN, title: String, price: Money } sig Customer { name: String, email: String, orders: set Order } sig Inventory { book: one Book, // 1つの本に対応 stock: Int, // 物理在庫数 reserved: Int // 予約済み数 } { stock >= 0 // 在庫は非負 reserved >= 0 // 予約数は非負 reserved <= stock // 予約数は在庫数を超えない }
25. #fp_matsuri Alloyによる構造的モデリング 25 書店システムの基本構造を定義 sig Order { customer: one Customer, items: set OrderItem, status: one OrderStatus, createdAt: Time } { some items // 注文には必ず商品が含まれる } sig OrderItem { book: one Book, quantity: Int, order: one Order } { quantity > 0 // 数量は正数 } abstract sig OrderStatus {} one sig Pending, Confirmed, Shipped, Cancelled extends OrderStatus {}
26. #fp_matsuri Alloyによる重要な制約の定義 26 ビジネスルールを数学的に表現 在庫整合性制約 // グローバルな不変条件 fact InventoryConsistency { // 確定済み注文の合計予約数 ≤ 在庫の予約数 all inv: Inventory | { let confirmedItems = { oi: OrderItem | oi.book = inv.book and oi.order.status = Confirmed } | let totalConfirmed = sum oi: confirmedItems | oi.quantity | inv.reserved >= totalConfirmed } }
27. #fp_matsuri Alloyによる重要な制約の定義 27 ビジネスルールを数学的に表現 オーバーブッキング防⽌制約 fact NoOverbooking { // すべての本について：確定注文の合計 ≤ 物理在庫 all b: Book | { let allConfirmedItems = { oi: OrderItem | oi.book = b and oi.order.status in (Confirmed + Shipped) } | let totalOrdered = sum oi: allConfirmedItems | oi.quantity | let currentStock = sum inv: Inventory | (inv.book = b) => inv.stock else 0 | totalOrdered <= currentStock } }
28. #fp_matsuri Alloyによる重要な制約の定義 28 ビジネスルールを数学的に表現 参照整合性制約 fact CustomerOrderRelation { // 注文と顧客の相互参照の整合性 all o: Order | o in o.customer.orders all c: Customer | all o: c.orders | o.customer = c } fact OrderItemConsistency { // 注文項目と注文の整合性 all oi: OrderItem | oi in oi.order.items all o: Order | all oi: o.items | oi.order = o }
29. #fp_matsuri Alloyによる問題発⾒の仕組み 29 モデル検査で何をチェックするか 1. Assertion（表明） - 成り⽴つべき性質 // 表明：在庫は決してマイナスにならない assert NoNegativeStock { all inv: Inventory | inv.stock >= 0 } // 表明：予約数は在庫数を超えない assert ReservationLimit { all inv: Inventory | inv.reserved <= inv.stock }
30. #fp_matsuri Alloyによる問題発⾒の仕組み 30 モデル検査で何をチェックするか 1. Assertion（表明） - 成り⽴つべき性質を検証 // 表明：確定注文には必ず在庫予約がある assert ConfirmedOrdersHaveReservations { all o: Order | o.status = Confirmed implies { all oi: o.items | { some inv: Inventory | inv.book = oi.book and inv.reserved >= oi.quantity } } }
31. #fp_matsuri Alloyによる問題発⾒の仕組み 31 モデル検査で何をチェックするか 2. Run コマンド - 問題のあるシナリオを探す // 在庫競合が発生する状況を探す run InventoryConflict { // 異なる2つの注文が同じ本を含む状況 some disj o1, o2: Order | o1.status = Pending and o2.status = Pending and some oi1: o1.items, oi2: o2.items | oi1.book = oi2.book } for 4 // 最大4個のオブジェクトで探索
32. #fp_matsuri Alloyによる具体的な問題発⾒例 32 検証の実⾏と結果の解釈 実際の検証コマンド // 1. 表明の検証 check NoNegativeStock for 5 check ReservationLimit for 5 check ConfirmedOrdersHaveReservations for 5 // 2. 問題シナリオの探索 run InventoryConflict for 4
33. #fp_matsuri Alloyによる具体的な問題発⾒例 33 検証の実⾏と結果の解釈 Alloy Analyzerが発⾒する問題例 🚨 発⾒された問題シナリオ1：同時注⽂での在庫競合の発⾒ Instance found: Book₀: isbn=ISBN₀, title="Kotlin Guide", price=Money₀ Customer₀: name="Alice", email="alice@example.com" Customer₁: name="Bob", email="bob@example.com" Inventory₀: book=Book₀, stock=1, reserved=0 Order₀: customer=Customer₀, status=Pending OrderItem₀: book=Book₀, quantity=1, order=Order₀ Order₁: customer=Customer₁, status=Pending OrderItem₁: book=Book₀, quantity=1, order=Order₁ // 問題：在庫1冊に対して2件の注文（計2冊）が存在 // どちらも確定されると在庫がマイナスになる
34. #fp_matsuri Alloyによる具体的な問題発⾒例 34 検証の実⾏と結果の解釈 Alloy Analyzerが発⾒する問題例 🚨 発⾒された問題シナリオ2：予約数の不整合 Instance found: Book₀: isbn=ISBN₀, title="Scala Book" Inventory₀: book=Book₀, stock=3, reserved=5 // 🚨 予約数が在庫数を超過 Order₀: status=Confirmed OrderItem₀: book=Book₀, quantity=2, order=Order₀ OrderItem₁: book=Book₀, quantity=3, order=Order₀ // 問題：物理在庫3冊なのに5冊予約されている状態 // reserved <= stock の制約に違反
35. #fp_matsuri Alloyによる具体的な問題発⾒例 35 検証の実⾏と結果の解釈 Alloy Analyzerが発⾒する問題例 Alloyが教えてくれること 🚨仕様の⽭盾: 定義した制約同⼠が⽭盾していないか 🚨エッジケース: 開発者が⾒落としがちな境界条件 🚨データの整合性: 関連するエンティティ間の参照整合性 🚨ビジネスルールの漏れ: 暗黙的な前提条件の明確化
36. #fp_matsuri 形式⼿法の基本⽂法（TLA+） 36 Alloyの基本構⽂要素 1. Variables（変数） - システムの状態 VARIABLES inventory, \* 各本の在庫数の関数 [BookId -> Nat] orders, \* 注文のシーケンス orderStatus, \* 各注文の状態 [OrderId -> Status] processing \* 現在処理中の注文集合 2. Constants（定数） - システムのパラメータ CONSTANTS Books, \* 本のIDの集合 Customers, \* 顧客のIDの集合 MaxStock, \* 最大在庫数 NULL \* null値を表す定数
37. #fp_matsuri 形式⼿法の基本⽂法（TLA+） 37 Alloyの基本構⽂要素 3. Type Invariant（型不変条件） - 変数の型制約 TypeInvariant == /\ inventory \in [Books -> Nat] \* 在庫は自然数の関数 /\ orders \in Seq([customer: Customers, book: Books, qty: Nat]) \* 注文はレコードのシーケンス /\ orderStatus \in [DOMAIN orders -> {"pending", "confirmed", "shipped", "cancelled"}] /\ processing \subseteq DOMAIN orders \* 処理中注文はOrderIdの部分集合 4. Actions（アクション） - 状態の変化 \* 新規注文の受付 PlaceOrder(customer, book, quantity) == /\ quantity > 0 \* 前提条件 /\ orders' = Append(orders, [customer |-> customer, book |-> book, qty |-> quantity]) /\ orderStatus' = Append(orderStatus, "pending") /\ UNCHANGED <<inventory, processing>> \* 他の変数は不変
38. #fp_matsuri TLA+の時間と状態遷移 38 状態遷移システムの記述 1. Initial State（初期状態） Init == /\ inventory = [b \in Books |-> MaxStock] \* すべての本の初期在庫 /\ orders = <<>> \* 空の注文リスト /\ orderStatus = <<>> \* 空の状態リスト /\ processing = {} \* 処理中注文なし
39. #fp_matsuri TLA+の時間と状態遷移 39 状態遷移システムの記述 2. State Transitions（状態遷移） \* 注文確定アクション（在庫チェック付き） ConfirmOrder(orderIndex) == /\ orderIndex \in DOMAIN orders \* 有効な注文インデックス /\ orderStatus[orderIndex] = "pending" \* 状態がpending /\ orderIndex \notin processing \* 処理中でない /\ LET order == orders[orderIndex] IN \* 該当注文を取得 /\ inventory[order.book] >= order.qty \* 在庫チェック /\ inventory' = [inventory EXCEPT ![order.book] = @ - order.qty] \* 在庫減算 /\ orderStatus' = [orderStatus EXCEPT ![orderIndex] = "confirmed"] /\ processing' = processing \cup {orderIndex}
40. #fp_matsuri TLA+の時間と状態遷移 40 状態遷移システムの記述 2. State Transitions（状態遷移） \* 注文キャンセルアクション CancelOrder(orderIndex) == /\ orderIndex \in DOMAIN orders /\ orderStatus[orderIndex] \in {"pending", "confirmed"} /\ IF orderStatus[orderIndex] = "confirmed" THEN inventory' = [inventory EXCEPT ![orders[orderIndex].book] = @ + orders[orderIndex].qty] ELSE UNCHANGED inventory /\ orderStatus' = [orderStatus EXCEPT ![orderIndex] = "cancelled"] /\ processing' = processing \ {orderIndex} /\ UNCHANGED orders
41. #fp_matsuri TLA+の時間と状態遷移 41 状態遷移システムの記述 3. Next State Relation（次状態関係） Next == \/ \E c \in Customers, b \in Books, q \in 1..10: PlaceOrder(c, b, q) \/ \E i \in DOMAIN orders: ConfirmOrder(i) \/ \E i \in DOMAIN orders: CancelOrder(i) \/ UNCHANGED <<inventory, orders, orderStatus, processing>> \* 何もしない遷移
42. #fp_matsuri TLA+による安全性と活性の検証 42 Safety Properties（安全性プロパティ）- 「悪いことは起こらない」 \* 在庫が負になることはない InventoryNeverNegative == \A b \in Books: inventory[b] >= 0 \* 確定済み注文の在庫は確保されている ConfirmedOrdersHaveStock == \A i \in DOMAIN orders: orderStatus[i] = "confirmed" => LET order == orders[i] IN inventory[order.book] >= 0
43. #fp_matsuri TLA+による安全性と活性の検証 43 Liveness Properties（活性プロパティ）- 「良いことは最終的に起こる」 \* すべての保留中注文は最終的に確定またはキャンセルされる OrdersEventuallyProcessed == \A i \in DOMAIN orders: orderStatus[i] = "pending" ~> orderStatus[i] \in {"confirmed", "cancelled"} \* 処理中の注文は最終的に完了する ProcessingEventuallyCompletes == \A i \in processing: orderStatus[i] = "confirmed" ~> orderStatus[i] \in {"shipped", "cancelled"} \* 在庫があれば注文は最終的に確定される StockAvailableImpliesConfirmation == \A i \in DOMAIN orders: /\ orderStatus[i] = "pending" /\ inventory[orders[i].book] >= orders[i].qty ~> orderStatus[i] = "confirmed"
44. #fp_matsuri TLA+による安全性と活性の検証 44 Specification（仕様）- 全体の動作定義 Spec == Init /\ [][Next]_<<inventory, orders, orderStatus, processing>> /\ WF_<<inventory, orders, orderStatus, processing>>(Next) \* WF (Weak Fairness): 条件が満たされ続けるなら、最終的にアクションが実行される
45. #fp_matsuri TLA+モデル検査による問題発⾒ 45 TLC（TLA+ Model Checker）による検証実⾏ \* モデル検査の範囲設定 CONSTANTS Books = {book1, book2, book3} Customers = {alice, bob, charlie} MaxStock = 5 NULL = "null" \* 検証したい性質 SPECIFICATION Spec INVARIANT TypeInvariant INVARIANT InventoryNeverNegative INVARIANT NoOverbooking PROPERTY OrdersEventuallyProcessed
46. #fp_matsuri TLA+モデル検査による問題発⾒ 46 TLCが発⾒する並⾏性問題の例 🚨 検証結果：安全性プロパティ違反 Behavior (counter-example trace): State 1: [Initial state] inventory = [book1 |-> 5, book2 |-> 5, book3 |-> 5] orders = <<>> orderStatus = <<>> processing = {} State 2: [PlaceOrder(alice, book1, 3)] orders = <<[customer |-> alice, book |-> book1, qty |-> 3]>> orderStatus = <<"pending">> State 3: [PlaceOrder(bob, book1, 3)] orders = <<[customer |-> alice, book |-> book1, qty |-> 3], [customer |-> bob, book |-> book1, qty |-> 3]>> orderStatus = <<"pending", "pending">>
47. #fp_matsuri TLA+モデル検査による問題発⾒ 47 TLCが発⾒する並⾏性問題の例 🚨 検証結果：安全性プロパティ違反 State 4: [ConfirmOrder(1)] // Alice's order confirmed inventory = [book1 |-> 2, book2 |-> 5, book3 |-> 5] orderStatus = <<"confirmed", "pending">> processing = {1} State 5: [ConfirmOrder(2)] // Bob's order confirmed inventory = [book1 |-> -1, book2 |-> 5, book3 |-> 5] 🚨 NEGATIVE! orderStatus = <<"confirmed", "confirmed">> processing = {1, 2} VIOLATION: InventoryNeverNegative violated at State 5 Total confirmed for book1 = 6, but MaxStock = 5
48. #fp_matsuri TLA+が発⾒する典型的な問題パターン 48 1. Race Condition（競合状態） \* 問題のあるシナリオ：2つの注文が同時に在庫をチェック State A: inventory[book1] = 1 Action 1: ConfirmOrder(order_alice_book1_qty1) - 在庫チェック通過 Action 2: ConfirmOrder(order_bob_book1_qty1) - 在庫チェック通過 Result: inventory[book1] = -1 🚨
49. #fp_matsuri TLA+が発⾒する典型的な問題パターン 49 2. Deadlock（デッドロック） \* 循環待機による処理停止 State: processing = {1, 2} Order 1 は Order 2 の完了を待つ Order 2 は Order 1 の完了を待つ → どちらも進まない状態
50. #fp_matsuri TLA+が発⾒する典型的な問題パターン 50 3. Livelock（ライブロック） \* 処理は進むが目標に到達しない 永続的に pending → confirmed → pending の繰り返し 注文が最終的に shipped に到達しない
51. #fp_matsuri AlloyとTLA+の使い分けと補完関係 51 AlloyとTLA+はAI駆動開発において補完的な存在になれる可能性 ツール Alloy TLA+ モデル対象 構造‧関係‧制約 動作‧時間‧並⾏性 検証内容 データモデル、不変条件 ワークフロー、並⾏処理 記述スタイル 宣⾔的‧制約ベース 状態遷移‧アクション 学習コスト 静的（時間の扱いなし） 動的（時系列あり） 出⼒ 反例‧インスタンス 状態遷移‧時系列
52. ⾃然⾔語仕様から形式⼿法への 変換プロセス例 52
53. #fp_matsuri ⾃然⾔語仕様から形式仕様への変換 53 ⾃然⾔語による初期要件（例） 【ステークホルダーによる⾔語化】 1. 顧客は本を検索して注⽂できる 2. 在庫がある本のみ注⽂可能 3. 注⽂後、在庫から商品を引き当てる 4. 同じ本を複数の顧客が同時に注⽂することがある 5. 在庫切れの場合は注⽂を受け付けない 6. 注⽂確定後はキャンセル可能 7. キャンセル時は在庫を復元する
54. #fp_matsuri ⾃然⾔語仕様から形式仕様への変換 54 ⾃然⾔語仕様にはらむ曖昧性 【⾃然⾔語で規定された仕様における曖昧性】 ❓ "在庫がある本のみ注⽂可能" → 在庫1冊に対して2件の同時注⽂は？ ❓ "同時に注⽂することがある" → 同時注⽂の処理順序は？ ❓ "在庫から商品を引き当てる" → 引き当てのタイミングは注⽂時？確定時？ ❓ "注⽂確定後はキャンセル可能" → 発送後もキャンセルできる？ ❓ "在庫を復元する" → 復元のタイミングは？他の待機注⽂への影響は？
55. #fp_matsuri ⾃然⾔語仕様から形式仕様への変換 55 形式検証による問題発⾒と明確化 Step 1: 曖昧性を含んだまま初期形式化 Alloy（構造的側⾯） sig Book { isbn: String, title: String } sig Customer { id: String } sig Order { customer: Customer, book: Book, quantity: Int, status: OrderStatus } abstract sig OrderStatus {} one sig Pending, Confirmed, Cancelled extends OrderStatus {} // 曖昧な制約（問題あり） fact VagueInventoryRule { // "在庫がある本のみ注文可能 " → 在庫の定義が曖昧 all o: Order | some book: Book | o.book = book // 何も制約していない }
56. #fp_matsuri ⾃然⾔語仕様から形式仕様への変換 56 形式検証による問題発⾒と明確化 Step 1: 曖昧性を含んだまま初期形式化 TLA+（動的側⾯） ProcessOrder(customer, book, quantity) == /\ "在庫チェック" \* 曖昧：どの時点での在庫？ /\ inventory[book] > 0 \* 問題：quantityを考慮していない /\ orders' = orders \cup {[customer |-> customer, book |-> book, qty |-> quantity]} /\ orderStatus' = [orderStatus EXCEPT ![Len(orders')] = "confirmed"] /\ inventory' = [inventory EXCEPT ![book] = @ - quantity] \* 危険：同時実行で競合
57. #fp_matsuri ⾃然⾔語仕様から形式仕様への変換 57 形式検証による問題発⾒と明確化 Step 2: 形式検証による問題発⾒ Alloyによる構造的問題の発⾒ run ConflictingOrders { some disj o1, o2: Order | o1.book = o2.book and o1.status = Confirmed and o2.status = Confirmed } for 3 // 結果：複数の注文が同じ本で確定される状況を生成 // → 在庫制約が不十分であることを発見
58. #fp_matsuri ⾃然⾔語仕様から形式仕様への変換 58 形式検証による問題発⾒と明確化 Step 2: 形式検証による問題発⾒ TLA+による並⾏性問題の発⾒ \* 2つの顧客が同時に最後の1冊を注文するシナリオ CONSTANTS alice = "Alice", bob = "Bob", book1 = "Book1" Init == /\ inventory = [book1 |-> 1] \* 在庫1冊 /\ orders = <<>> \* TLC検査結果： \* Error: Invariant violated \* State 1: inventory[book1] = 1 \* Action: ProcessOrder(alice, book1, 1) \* State 2: inventory[book1] = 0, orders contains alice's order \* Action: ProcessOrder(bob, book1, 1) \* 同時実行 \* State 3: inventory[book1] = -1 \* 在庫がマイナス！
59. #fp_matsuri ⾃然⾔語仕様から形式仕様への変換 59 形式検証による問題発⾒と明確化 Step 3: 統合的な制約明確化 Alloyでの構造制約の精緻化 sig Inventory { book: one Book, availableStock: Int, reservedStock: Int } { availableStock >= 0 reservedStock >= 0 } fact ClearInventoryConstraint { // 明確化：確定注文の合計は利用可能在庫を超えない all b: Book | { let totalConfirmed = sum o: Order | (o.book = b and o.status = Confirmed) => o.quantity else 0 | let inventory = { inv: Inventory | inv.book = b } | all inv: inventory | totalConfirmed <= inv.availableStock
60. #fp_matsuri ⾃然⾔語仕様から形式仕様への変換 60 形式検証による問題発⾒と明確化 Step 3: 統合的な制約明確化 TLA+での並⾏制御の明確化 \* 修正版：原子的な在庫チェックと更新 ProcessOrderAtomic(customer, book, quantity) == /\ \neg orderLock[book] \* 排他制御：ロックされていない /\ inventory[book] >= quantity \* 十分な在庫があることを確認 /\ orderLock' = [orderLock EXCEPT ![book] = TRUE] \* ロック取得 /\ inventory' = [inventory EXCEPT ![book] = @ - quantity] /\ orders' = Append(orders, [customer |-> customer, book |-> book, qty |-> quantity]) /\ orderStatus' = Append(orderStatus, "confirmed") /\ orderLock'' = [orderLock' EXCEPT ![book] = FALSE] \* ロック解放 \* 並行安全性の保証 ConcurrentOrderingSafety == \A b \in Books: Cardinality({o \in ProcessingOrders : o.book = b}) <= 1
61. #fp_matsuri ⾃然⾔語仕様から形式仕様への変換 61 明確化された統合仕様 【形式検証後の明確化された仕様】 1. 構造的制約（Alloyで検証済み）： - 各本には物理在庫数と予約済み在庫数がある - 利⽤可能在庫 = 物理在庫 - 予約済み在庫 - 予約済み在庫 = 確定済み注⽂の合計数
62. #fp_matsuri ⾃然⾔語仕様から形式仕様への変換 62 明確化された統合仕様 【形式検証後の明確化された仕様】 2. 動的制約（TLA+で検証済み）： - 注⽂処理は原⼦的操作として実⾏ - 在庫チェックと予約は同⼀トランザクション内 - 同じ本への同時注⽂は排他制御で順次処理
63. #fp_matsuri ⾃然⾔語仕様から形式仕様への変換 63 明確化された統合仕様 【形式検証後の明確化された仕様】 3. 統合制約（両⽅で検証済み）： - 確定注⽂の合計は初期在庫を絶対に超えない - すべての状態でデータ整合性が保たれる - 並⾏処理でも安全性が保証される
64. #fp_matsuri ⾃然⾔語仕様から形式仕様への変換 64 形式検証の価値：発⾒から解決まで 🔍 Alloyが発⾒: 「在庫の概念が曖昧」「予約数の定義が不明確」 🔍 TLA+が発⾒: 「同時処理で競合発⽣」「原⼦性の⽋如」 ✅ 統合的解決: 「構造的制約 + 動的制御 = 完全な安全性」 従来のアプローチ: 実装後にバグ発⾒ → 修正 → ⼿戻り 形式⼿法: 実装前に問題発⾒ → 仕様明確化 → 安全な実装（シフトレフト）
65. 代数的データ型‧関数型ドメインモデリング による型安全な実装 65
66. #fp_matsuri 形式仕様からコードへの橋渡し 66 なぜ代数的データ型（ADT）が重要なのか？ Alloyで定義した制約をコードでどう表現するか？ // Alloyでの制約定義 abstract sig OrderStatus {} one sig Pending, Confirmed, Shipped, Cancelled extends OrderStatus {} fact StatusConstraints { all o: Order { o.status = Confirmed implies some o.approvals // 確定には承認が必要 o.status = Shipped implies o.status.prev = Confirmed // 発送前に確定必須 } }
67. #fp_matsuri 形式仕様からコードへの橋渡し 67 なぜ代数的データ型（ADT）が重要なのか？ ただのenum等では適切に制約を表現できない // 型システムで制約を表現できない enum class OrderStatus { PENDING, CONFIRMED, SHIPPED } var approvals: List<Approval>? = null // いつ必要？ 関数型プログラミングの解：代数的データ型 // 制約を型システムに直接埋め込み sealed class OrderStatus // Sum Type（直和型） data class Confirmed(val approvals: List<Approval>) // Product Type（直積型）
68. #fp_matsuri 代数的データ型 68 ADTの2つの基本構成要素 1. Sum Type（直和型） - OR の関係 sealed class PaymentMethod { data class CreditCard(val number: String, val expiry: String) : PaymentMethod() data class BankTransfer(val accountNumber: String) : PaymentMethod() object Cash : PaymentMethod() } // PaymentMethod = CreditCard OR BankTransfer OR Cash 2. Product Type（直積型） - AND の関係 data class Address( // すべてのフィールドが必要 val street: String, // street AND val city: String, // city AND val zipCode: String // zipCode ) // Address = street AND city AND zipCode
69. #fp_matsuri 代数的データ型 69 組み合わせることで複雑な制約を表現 sealed class OrderStatus { object Pending : OrderStatus() // 単純な状態 // Product Typeで必要なデータをまとめる data class Confirmed( val confirmedAt: Instant, // 確定日時 val reservedInventory: Reservation, // 在庫予約 val approvals: NonEmptyList<Approval> // 必須の承認リスト ) : OrderStatus() }
70. #fp_matsuri 関数型ドメインモデリングの実践 70 1. 不可能な状態を型で表現不可能にする 悪い例：無効な状態が作れてしまう data class Order( val id: OrderId, val status: String, // 文字列では制約なし val items: List<OrderItem>, // 空リストが可能 val total: Money, // itemsと不整合の可能性 val customerId: String? // 顧客なしの注文が可能？ ) // 無効な状態が作成可能 val invalidOrder = Order( id = OrderId("123"), status = "UNKNOWN_STATUS", // 存在しない状態 items = emptyList(), // 商品のない注文 total = Money(100), // itemsと矛盾 customerId = null // 顧客不明 )
71. #fp_matsuri 関数型ドメインモデリングの実践 71 1. 不可能な状態を型で表現不可能にする 良い例：型システムで制約を強制 data class Order private constructor( val id: OrderId, val customerId: CustomerId, // NonNull、専用型 val items: NonEmptyList<OrderItem>, // 必ず1つ以上 val status: OrderStatus // 有効な状態のみ ) { companion object { fun create(customerId: CustomerId, items: NonEmptyList<OrderItem>): Order { require(items.isNotEmpty()) { "Order must have items" } return Order(OrderId.generate(), customerId, items, OrderStatus.Pending) } } // 計算プロパティで常に整合性保証 val total: Money get() = items.sumOf { it.subtotal } }
72. #fp_matsuri 関数型ドメインモデリングの実践 72 2. 状態遷移の制約を型レベルで表現 // 型安全な状態遷移 fun Order.ship(trackingNumber: TrackingNumber, carrier: ShippingCarrier): Either<OrderError, Order> = when (val currentStatus = this.status) { is OrderStatus.Confirmed -> { val shippedStatus = OrderStatus.Shipped( shippedAt = Instant.now(), trackingNumber = trackingNumber, carrier = carrier, previousState = currentStatus // 型で制約 ) Either.Right(this.copy(status = shippedStatus)) } else -> Either.Left(OrderError.InvalidTransition( "Cannot ship order in ${currentStatus::class.simpleName} status" )) }
73. #fp_matsuri 関数型ドメインモデリングの実践 73 3. プリミティブ型を避け、ドメイン概念を型で表現 // 型安全な関数シグネチャ fun processPayment( amount: Money, // 金額の型が明確 customerId: CustomerId, // 顧客IDとして明示 orderId: OrderId // 注文IDとして明示 ): PaymentResult = // 引数の順序を間違えてもコンパイルエラー paymentGateway.charge(amount, customerId, orderId)
74. プロパティベーステスト による性質のテスト 74
75. #fp_matsuri プロパティベーステスト 75 制約をテストで検証 @Property fun `在庫は決してマイナスにならない `( @ForAll("positiveStock") initialStock: StockQuantity, @ForAll("stockOperations") operations: List<StockOperation> ) { val inventory = Inventory(sampleBook, initialStock, StockQuantity.ZERO) val finalInventory = operations.fold(inventory) { inv, op -> when (op) { is StockOperation.Reserve -> inv.reserve(op.quantity).getOrElse { inv } is StockOperation.Release -> inv.release(op.quantity) is StockOperation.Restock -> inv.restock(op.quantity) } } assertThat(finalInventory.physicalStock.value).isGreaterThanOrEqualTo(0) assertThat(finalInventory.reservedCount.value).isGreaterThanOrEqualTo(0) assertThat(finalInventory.reservedCount.value) .isLessThanOrEqualTo(finalInventory.physicalStock.value) }
76. #fp_matsuri プロパティベーステスト 76 ⾼度なプロパティテストパターン ラウンドトリップテスト（Roundtrip Properties Test） "注文のシリアライズ・デシリアライズ " { checkAll<Order> { originalOrder -> val serialized = orderSerializer.serialize(originalOrder) val deserialized = orderSerializer.deserialize(serialized) deserialized shouldBe originalOrder // ラウンドトリップで元に戻る } } "注文追加と削除の逆操作" { checkAll<Order, OrderItem> { order, item -> val withItem = order.addItem(item).getOrNull() val withoutItem = withItem?.removeItem(item.bookId) withoutItem shouldBe order // 追加→削除で元に戻る } }
77. #fp_matsuri プロパティベーステスト 77 ⾼度なプロパティテストパターン メタモルフィックテスト（Metamorphic Test） "配送料計算の単調性" { checkAll<Order, OrderItem> { order, additionalItem -> val originalShippingCost = shippingService.calculateCost(order) val expandedOrder = order.addItem(additionalItem).getOrNull() val newShippingCost = expandedOrder?.let { shippingService.calculateCost(it) } // 商品を追加しても配送料は減らない（単調性） newShippingCost?.let { it shouldBeGreaterThanOrEqual originalShippingCost } }
78. #fp_matsuri プロパティベーステスト 78 ⾼度なプロパティテストパターン 不変条件の維持（Invariant Properties） "どんな操作をしても在庫の不変条件は維持される " { checkAll<BookInventory, List<InventoryOperation>> { initialInventory, operations -> val finalInventory = operations.fold(initialInventory) { inventory, operation -> when (operation) { is InventoryOperation.Reserve -> inventory.reserve(operation.quantity).getOrElse { inventory } is InventoryOperation.Cancel -> inventory.cancel(operation.reservationId).getOrElse { inventory } is InventoryOperation.Restock -> inventory.restock(operation.quantity).getOrElse { inventory } } } // 不変条件の検証 finalInventory.physicalStock shouldBeGreaterThanOrEqual 0 finalInventory.reservedStock shouldBeGreaterThanOrEqual 0 finalInventory.reservedStock shouldBeLessThanOrEqual finalInventory.physicalStock finalInventory.availableStock shouldBe (finalInventory.physicalStock - finalInventory.reservedStock) } }
79. AIコーディングエージェントとの協業 79
80. #fp_matsuri 実際にAI駆動設計に当てはめてみる 80 AIエージェントに形式⼿法により明確化された仕様と⽅針をわたす（簡易版） 以下のAlloy仕様に基づいて、Kotlinで型安全な実装を⽣成してください： ## 制約 1. NoOverbooking: 総注⽂数 ≤ 物理在庫 2. AtomicAllocation: 在庫引き当ては原⼦的操作 3. PositiveStock: 在庫は常に⾮負 ## 要求 - sealed classで注⽂状態を表現 - Either型でエラーハンドリング - プロパティベーステストを含める [Alloy仕様全⽂を添付]
81. #fp_matsuri AI駆動開発と形式⼿法‧関数型モデリングの可能性 81 究極的なシフトレフトをAIの⼒で加速する シフトレフト（開発プロセスの早期フェーズでの問題発⾒）アプローチ 従来: 要件 → 設計 → 実装 → テスト → [バグ発⾒] → 修正  ↑ ⾼コストなフェーズでバグ発⾒ 改善: [形式仕様] → AIコード⽣成 → [プロパティテスト] → デプロイ ↑ ↑ 早期にバグ防⽌ 継続的な制約検証と関数型‧型による堅牢化
82. #fp_matsuri AI駆動開発の⼤きな可能性（最新情報） 82 Claude Code (with Claude 4 Opus/Sonnet)でのAI駆動開発の現状 • ⾃然⾔語で作成したPRD（プロダクト要求仕様書）をClaude Codeに渡して開発をトライしたと ころ、通常エンジニア2~3名チームでおおよそ2‧3週間かかる⼯程の作業が3⽇で終了 • 仕様の品質向上、レビューや検証の質‧スピード向上をいかに実現できるかが重要 ‐ PRDの段階で不明瞭だったものがそのままアウトプットの質低下に寄与する ‐ シフトレフトをいかに実現できるかが最終的な質とスピード向上に効いてくる • 形式⼿法のアプローチはまだ実践導⼊できていないが、⼤いなる可能性を感じている
83. #fp_matsuri 本⽇お話ししたアプローチ 🎯 Alloy/TLA+による仕様の厳密化 → 曖昧な⾃然⾔語要件から数学的に検証可能な仕様へ 🎯 代数的データ型‧関数型ドメインモデリングによる型安全な実装 → 形式仕様の制約を型レベルで直接表現 🎯 プロパティベーステストによる継続的検証 → 仕様適合性の⾃動確認 🎯 AI駆動開発に上記を組み込むことによるシフトレフトの実現 → ガードレールとしての制約を設けることでAIがその枠内で全⼒でパフォーマンスを発揮できる可能性の提⽰ まとめ 83