形式的手法の基礎と応用

付録D：演習問題解答

本文の演習問題の代表的な解答例と解説を掲載します。段階的なヒントとチェックポイントを含める予定です。

注意事項

  • 本付録の疑似スクリプト・ログ構造・設定例は、理解を助けるための例示です。実運用ではプロジェクトの環境・要件に合わせて調整してください。
  • 用語や図表番号は本文と対応させています。引用時は該当章・図の参照（例: 図10-1, 図11-1）を明記してください。

解答の読み方（共通）

  • 骨子→模範解答の流れ：章末に示した「解答の方向性（骨子）」に沿って、最小限の根拠と用語整合を確認
  • 採点観点：各章末の採点観点に対応。網羅性/一貫性/再現性/妥当性を重視

サンプル（第2章 問1）

  • 選定：Alloy（初期導入/反例探索）＋TLA+（分散の安全/活性）
  • 理由（要約）：構造整合の早期発見はAlloyの小スコープ反例が有効。分散性質はTLA+の安全/活性で段階的に担保

チェックポイント

  • 比較軸が3観点を満たすか、選定と文脈の一貫性
  • 導入段階/CI配置（PR/夜間/リリース前）への落とし込み可否

サンプル（第8章 問1）

  • 最小反例（例）: 初期 Q=[], Enqueue(1), Enqueue(2), Dequeue(), Dequeue() → FIFO逸脱
  • 前提: 単一キュー/単一消費/境界条件（空時のDequeue禁止）

チェックポイント

  • 反例トレースの再現性（seed/深さ固定）
  • 境界条件・前提の明示と妥当性

サンプル（第3章 問1）

  • UML制約例: 「顧客は0個以上の注文を持つ（多重度 0..*）」「1つの注文はちょうど1人の顧客に属する（多重度 1）」
  • 写像の要点（Alloy例）:
    • 集合: sig Customer { orders: set Order }、sig Order { owner: one Customer }
    • 制約: fact Ownership { all o: Order | one o.owner and o in o.owner.orders }

チェックポイント

  • 多重度の整合（one/set）と双方参照の一貫性
  • 不変（fact）として常時成立に置くか、性質（assert）で検査するかの使い分け

サンプル（第4章 問2）

  • 診断順序: 1) 制約の過不足（弱すぎ/強すぎ）→ 2) スコープ（過小/過大）→ 3) 抽象度（過度な単純化）
  • 例: 反例で循環が報告 → acyclic 制約の追加/修正を優先（制約適正化）

チェックポイント

  • 反例の根因に近い制約から手当てすること（スコープ調整は副作用が大きい）
  • 修正後の再検証と回帰防止（assertの追加）

サンプル（第5章 問1）

  • 影響の整理:
    • 事前条件: 不変追加により操作の適用可能条件が強化される可能性
    • 事後条件: 新不変の充足を保証する追加義務（更新式の見直し）

チェックポイント

  • ' 付き変数の整合（更新前後の対応）
  • 前提強化による到達不能操作の検出と方針（分割/緩和）

サンプル（第6章 問1/問2）

  • 問1（最小デッドロック例）: P1 は ch1!a → ch2?b、P2 は ch2!b → ch1?a を順に要求。相互待ちで停止。
  • 回避策: 送受順の合意（全体順序）/一方向化/タイムアウト付きリトライ/有限バッファで背圧維持

チェックポイント

  • 競合の原因（同時双方向同期）を特定し、プロトコルの順序/同期形態の見直しで解消

  • バッファ導入時の副作用（順序逆転/無限滞留）の検討

  • 問2（非同期化の副作用）: 無限バッファは背圧喪失により生産過多→消費追従不可で遅延/メモリ肥大

チェックポイント

  • 進行性/安全性の両観点（失敗・ダイバージェンス）で評価
  • 上限/ドロップ戦略/優先度制御などの設計を明記

サンプル（第7章 問1/問2）

  • 問1（相互排他の状態/不変）: 変数 turn, flag[2]。不変: ¬(crit[0] ∧ crit[1])、公正性: 各プロセスは無限に機会を得る

チェックポイント

  • クリティカル区間の定義と進行性仮定（弱/強公正）の選択

  • 初期化・遷移で不変が保存されることを確認

  • 問2（損失チャネルでの到達性崩れ）: send が落ちると ack 不達→再送/ACK/タイムアウト追加で eventually-delivery を高める

チェックポイント

  • 環境仮定（損失の確率/上限）と公正性との関係
  • 再送戦略の停止条件と重複抑止（idempotence）の設計

サンプル（第11章 問1/問2）

  • 問1（PR段階の最小検証）: 目的=早期フィードバック/再現性。実行≤90秒、seed固定、小スコープAlloy/TLC/契約チェックのいずれか1–2個。
  • 失敗時の扱い: 反例トレース/再現スクリプト/影響範囲（仕様/実装/環境）を自動添付

チェックポイント

  • 速度/安定性/再現性の3条件を満たす構成

  • チームが再現→修正→再検証のループを実行できること

  • 問2（リリース前ゲート）: クリティカル性質=証明/長時間TLC。システム性=模型検査。実装整合=契約。ゲート条件は強制/ソフトを性質毎に使い分け

チェックポイント

  • 性質と手法の適合、制限時間と確実性のバランス
  • 例外時の承認フローとロールバック条件の定義

付録テンプレ（リリース前ゲート例外フロー）

  • 例外申請条件: 「非クリティカル性質のみ未達」「代替検証/運用緩和策あり」「影響範囲が限定」
  • 申請内容: 未達性質/根因/代替策/フォローアップ計画（期限/担当）
  • 承認者: 技術責任者＋プロダクト責任者（ダブルチェック）
  • リリース後フォロー: 期限内に性質を回復（検証強化/仕様改修）し、回帰検証を実施
  • ロールバック条件: 監視指標のしきい値超過/代替策の効果不十分時に即時切り戻し

サンプル（第12章 問1）

  • 目標: PR/夜間/リリース前で検証深度を段階化し、速度と保証のバランスを取る
  • 構成（疑似YAML要約）:
    • PR: 小スコープAlloy（≤60s）、TLC短時間（≤60s）、契約チェック（fast）
    • 夜間: Alloyスコープ拡大、TLC深さ拡大、CSPモデル検査（時間上限長め）
    • リリース前: クリティカル性質の証明/長時間TLC、レビュー付き承認

チェックポイント

  • PRの合計時間≤90秒、seed固定でflake対策、失敗時の反例自動添付
  • 夜間で偽陰性低減（探索深度/スコープ拡大）、リソースと並列度の管理
  • リリース前の強制/ソフトゲートの整理と例外フロー（第11章テンプレ参照）

サンプル（第10章 問2）

  • ループ不変の例: 「配列の先頭からi未満は昇順」
  • 追加前提: 1) 初期化で不変が成り立つ、2) 本体で不変が維持される、3) 終了性: 変位関数 n-i が自然数で単調減少

チェックポイント

  • 三点チェック（初期化/保持/終了）の明示
  • 減少関数や良基順序の明確化