付録D：演習問題解答（ヒント/模範解答/採点観点）

本付録は、各章末課題に対して「提出物として何を作るか」を明確にするためのテンプレート集です。 章末課題の性質上、模範解答は一意ではないため、ここでは 解答の骨子（最小構成）と 採点観点（rubric） を中心に示します。

注意事項

• 本付録の疑似スクリプト・ログ構造・設定例は例示です。実運用ではプロジェクトの環境・要件に合わせて調整してください。
• 数字（%/倍/件数）は出典を付与するか、例示であることを明示してください。

D.1 共通：提出物テンプレと採点観点

共通の提出物（推奨）

• 問題設定：対象、前提、境界（in-scope/out-of-scope）
• 仕様：用語定義、前提条件、性質（安全/活性/契約）
• 検証：実行コマンド、設定（seed/深さ/スコープ/上限時間）、結果ログ
• 反例対応（発生時）：最小トレース、原因仮説、修正差分、再検証ログ（付録F.8参照）

共通の採点観点（rubric）

• 正確性：定義・制約・推論が整合している
• 完全性：要求を満たす観点が落ちていない（例外/境界条件を含む）
• 一貫性：用語・記号・抽象化レベルが揃っている
• 再現性：第三者が同じ手順で再実行できる（コマンド・設定・ログ）
• 妥当性：前提条件（環境仮定、障害モデル、性能制約）が明示されている

D.2 第1章

思考演習1：複雑性分析

ヒント（段階）

1. 対象システムの境界（外部API/依存先/運用）を確定する
2. 構成要素と相互作用を列挙し、組み合わせ爆発の観点（状態数・遷移数）で整理する
3. 失敗モード（部分故障/競合/仕様齟齬）を洗い出し、SIL相当の要求水準を仮置きする

模範解答（骨子）

• コンポーネント一覧（役割/責務）と相互作用図
• 状態・遷移の「増え方」の評価（どの部分が爆発するか）
• 失敗モードと安全性要求（SIL相当）の根拠

採点観点

• 境界が明確（前提の抜けが少ない）
• 複雑性を「相互作用」と「状態空間」で説明できる
• 失敗モードが具体（運用を含む）

実践演習：事故分析と予防策検討

ヒント（段階）

1. 事故の直接原因/根本原因を「仕様」「実装」「運用」「組織」に分解する
2. どの性質（不変/契約/安全性/活性）が破れたかを言語化する
3. Alloy/TLA+/プログラム検証のどれで「どの抽象度」を先に潰せるかを整理する

模範解答（骨子）

• 原因分析（技術/組織）と、仕様曖昧性の寄与
• 予防可能性のマッピング（第4/8/10章の手法に対応付け）
• 現代の同型リスクと、業務上の予防アクション

採点観点

• 事故要因の分解が妥当
• 「検証可能な性質」へ落ちている
• 提案が具体（導入ステップ/検証ゲート/例外フロー）

実践演習：仕様曖昧性の定量的分析

ヒント（段階）

1. 曖昧語を列挙し、解釈の分岐点（例：回数制限、失敗の定義、エラーメッセージ粒度）を分ける
2. 実装バリエーションは「分岐の積」として概算する（厳密な数でなく、説明可能な見積りでよい）
3. セキュリティ上のリスクは、攻撃面・観測可能性・誤作動影響で三段階評価する

模範解答（骨子）

• 曖昧性一覧表（曖昧箇所/解釈候補/分岐数/影響）
• 実装パターン総数の概算と計算根拠
• 優先順位付け（第3章の仕様化で先に潰す項目）

採点観点

• 曖昧性の抽出が十分
• 見積り根拠が明示されている
• セキュリティ観点が入っている

発展演習：業務適用計画の立案

ヒント（段階）

1. 適用候補は「失敗コストが高い」「仕様が曖昧」「並行/分散がある」から選ぶ
2. 学習する章（3章程度）の選定は「自分の業務で再現できる」順に決める
3. 提案資料は、ROI（第11章）と段階導入（PR/夜間/リリース前）で合意形成する

模範解答（骨子）

• 適用候補（範囲/期待効果/リスク）の整理
• 6ヶ月/1年の学習と実践計画（成果物とKPI）
• 組織提案（投資対効果、ガードレール、例外フロー）

採点観点

• 対象選定が合理的
• 成果物とKPIが具体
• 組織への説明が現実的

D.3 第2章

理解確認演習1：データ構造の集合論的表現

ヒント（段階）

1. Studentの型を直積で定義する（Name×Age×Courses）
2. Coursesは「集合/列/多重集合」のどれとして扱うかを明確化する
3. 「履修している」関係を Student ↔ Course で定義する

模範解答（骨子）

• Student == Name × Nat × P(Course)（例：Coursesを集合として扱う場合）
• students ⊆ Student（例：集合として扱う場合。順序が重要なら列として扱う）
• enrolled ⊆ Student × Course と所属判定 ⟨s,c⟩ ∈ enrolled

採点観点

• 型の選択が一貫している
• 関係/写像の使い分けが妥当
• 境界（順序/重複の扱い）が明示されている

理解確認演習2：論理と制御構造

ヒント（段階）

1. 自然言語条件を命題（P,Q,…)へ分解し、論理式へ変換する
2. 量化（∀/∃）は集合境界（ユーザー集合、商品集合）を明示する
3. 実装条件式では、null/未設定/例外の扱いも前提として書く

模範解答（骨子）

• 例：canDrive ⇔ (age>=18) ∧ hasValidLicense
• 例：canDelete ⇔ isAdmin ∨ isOwner
• 例：∀u ∈ Users : hasValidEmail(u)
• 例：∃p ∈ Products : inStock(p)

採点観点

• 論理式が要件を過不足なく表現
• 量化範囲が明示
• 実装への落とし込みで例外が考慮されている

実践演習：状態モデリング

ヒント（段階）

1. 状態変数（投入金額、選択、在庫、返却金）を最小で定義する
2. 入力イベント（投入/選択/キャンセル）ごとに遷移を定義する
3. 不変条件は「金額保存」「在庫非負」「不正遷移がない」から作る

模範解答（骨子）

• 状態：balance, stock, selected, change など
• 入力集合：Insert100|Insert500|SelectCola|SelectTea|Cancel など
• 不変条件例：balance>=0、stock[item]>=0、purchase => balance>=price

採点観点

• 状態空間と入力が網羅的
• 不変条件が要求と対応
• シナリオが遷移列として一貫している

発展演習：並行性の分析

ヒント（段階）

1. 取引を「読み→計算→書き」と分解して遷移化する
2. インターリービングを列挙し、保存すべき性質（残高非負/保存則）を見る
3. 制約案は「排他」「原子操作」「再試行」「順序化」から選ぶ

模範解答（骨子）

• インターリービングにより lost update が起こる例の提示
• 不整合条件（例：最終残高が順次実行と一致しない）
• 制約案（ロック、トランザクション、CAS等）

採点観点

• インターリービングが正しく列挙されている
• 不整合の発生条件が説明できる
• 制約が副作用込みで妥当

統合演習：形式的手法への準備

ヒント（段階）

1. まず「集合・関係・不変」を自然言語で固定し、手法に写像する
2. Alloy/Z/CSP/TLA+のどれが何を得意とするか（図2-2）で役割分担する

模範解答（骨子）

• 演習1（Alloy）：エンティティ/関係/制約（管理者が少なくとも1人等）を sig/fact/assert に割当
• 演習2（Z）：状態スキーマ＋操作スキーマ（正常/エラー）を定義し、事前/事後条件を分離
• 演習3（CSP）：プロセス/チャネル/順序制約を定義し、デッドロック観点を列挙
• 演習4（TLA+）：状態変数/安全性/活性/公正性仮定を分けて記述

採点観点

• 手法の割当が合理的
• 不変/活性/例外の観点が含まれる
• 後続章への接続（何を作るか）が明確

D.4 第3章

基礎理解演習1：曖昧性の特定

ヒント（段階）

1. 「適切に」「大きすぎる」「不正な」など、閾値や判定主体が不明な語を列挙
2. それぞれの解釈が設計・運用（ログ/監査/再試行）に与える影響を整理

模範解答（骨子）

• 曖昧語→解釈候補→影響（誤検知/漏検知/UX/運用負荷）の表
• 仕様化で確定すべき項目の優先順位

採点観点

• 曖昧性が十分に抽出されている
• 影響が実装/運用まで含む

基礎理解演習2：契約の記述

ヒント（段階）

1. 事前条件：入力が「探索可能」である条件（ソート済み、範囲）
2. 事後条件：返り値が満たす性質（見つかる/見つからない）
3. フレーム条件：変更されない（配列不変）を明示

模範解答（骨子）

• pre：sorted(sorted_array)、sorted_array != null
• post（found）：0<=ret<n ∧ sorted_array[ret]=target
• post（not found）：ret=-1 ∧ ∀i. sorted_array[i] != target
• frame：sorted_array は変更されない

採点観点

• pre/post/frame が分離されている
• 返り値の条件が両ケースで完結している

実践演習1：キューの仕様化

ヒント（段階）

1. 状態は「列（sequence）」として表すとFIFOが書きやすい
2. 操作ごとに、状態更新と戻り値の関係を定義する
3. エラー（空dequeue等）は事前条件か例外ケースで扱う

模範解答（骨子）

• 状態：Q（列）
• enqueue：Q' = Append(Q, x)
• dequeue（非空）：ret = Head(Q) ∧ Q' = Tail(Q)
• isEmpty/size/front の定義
• 不変：size(Q) >= 0、（必要なら）要素型制約

採点観点

• FIFOが仕様に反映されている
• 事前条件/例外が明確
• 操作間整合（front/dequeue）が保たれる

実践演習2：電子メールシステムの不変条件

ヒント（段階）

1. データ整合性（参照一貫性、重複排除）を先に定義する
2. セキュリティ（認証情報、アクセス制御）を不変として切り出す
3. ビジネスルール（メールの所属、ゴミ箱移動等）を追加する

模範解答（骨子）

• 整合性例：メールアドレス一意、メッセージの送信者/受信者がユーザー集合に属する
• セキュリティ例：パスワード平文禁止（ハッシュ化前提）、ログイン必須で操作可能
• ルール例：メッセージは（受信/送信/ゴミ箱）のいずれかに所属、同一メッセージIDの重複禁止

採点観点

• 不変がカテゴリ分けされている
• 参照関係が破れない
• 例外（削除/移動/未配達）が考慮されている

発展演習：仕様の検証

ヒント（段階）

1. 一貫性：操作の合成（enqueue→dequeue等）で矛盾が出ないか
2. 完全性：利用パターン（空/満杯/境界）を列挙
3. テスト戦略：仕様→テスト観点（境界/同値分割/反例）へ写像

模範解答（骨子）

• 仕様レビュー観点のチェックリスト
• 実装可能性（計算量/データ構造）に関する注記
• テストケース設計の骨子

採点観点

• 検証観点が体系化されている
• 仕様→テストが接続できている

D.5 第4章

基礎演習1：Alloyモデルの読解

ヒント（段階）

1. lone/set/one の多重度が意味する制約を言語化する
2. fact は常に成立する制約、assert は検査対象（反例探索）として使い分ける
3. 不足制約（自己配偶の禁止、親子循環の禁止等）を検討する

模範解答（骨子）

• spouse: lone Person は「高々1人の配偶者」
• parents/children の双方向整合
• 欠けている可能性：p.spouse != p、親子関係の非循環、配偶者は相互排他的（重婚禁止）など

採点観点

• 各制約の意味が説明できる
• 妥当性（業務要件との差）を述べられる

基礎演習2：制約の記述

ヒント（段階）

1. User/Book/Loan を分離し、貸出は関係（またはLoan）として表す
2. 「最大5冊」「延滞不可」などのルールは fact として固定する
3. 返却期限は抽象化（Dateの順序は省略し、期限超過フラグ等で表す）してよい

模範解答（骨子）

• sig User { loans: set Loan }, sig Book {} など
• fact UniqueLoan { all b: Book | lone l: Loan | l.book = b }
• fact Limit { all u: User | #u.loans <= 5 }
• fact Overdue { all u: User | u.overdue => no u.newLoan }（例）

採点観点

• 要求が過不足なく制約化されている
• 抽象化の前提が明示されている

実践演習1：セキュリティポリシーのモデル化

ヒント（段階）

1. アクセス判定は述語 canRead/canWrite として切り出す
2. fact は不変、assert は「破れてはいけない性質」を置く
3. 管理者特権は例外として明示する（優先順位も含む）

模範解答（骨子）

• sig User { groups: set Group }, sig File { owner: one User, mode: one Mode, sharedWith: set Group }
• pred canWrite[u,f] { u=f.owner or u in Admins and f.mode=RW ... }
• assert NoWriteToRO { all u,f | f.mode=RO implies not canWrite[u,f] }

採点観点

• 権限モデルが矛盾しない
• assertが要件と対応している

実践演習2：模型検査と改善

ヒント（段階）

1. run でインスタンス生成→現実的/不自然な例を把握
2. check とスコープ変更で反例を得る（小スコープ優先）
3. 修正は「制約の過不足」から順に行い、再検証と回帰（assert追加）を行う

模範解答（骨子）

• 反例ログ（最小）と、何が破れたかの説明
• 原因仮説→制約修正→再検証の履歴

採点観点

• 反例を事実として扱い、推測と分離できている
• 修正が最小で、回帰防止がある

発展演習：動的振る舞いのモデル化

ヒント（段階）

1. 時刻（ステップ）を sig Time 等で表現し、状態を balance: Time -> Account -> Int などで持つ
2. 操作を pred Withdraw[t,t'] の形式で書き、保存則を不変として置く

模範解答（骨子）

• 状態変数（残高、履歴）と操作（入出金）の定義
• 不変：残高非負、総額保存（モデル境界内）、履歴整合

採点観点

• 状態と操作が時間で接続している
• 不変が検証可能な形で定義されている

D.6 第5章

基礎理解演習1：スキーマの読解と分析

ヒント（段階）

1. 型（集合/関係/部分関数）を読み取り、dom/ran制約の意味を説明する
2. 制約は「参照整合」と「存在保証」に分解する

模範解答（骨子）

• 変数の型と意味（students/courses/enrollment等）
• dom enrollment ⊆ students 等の整合性制約の説明
• 表現できない要求（例：最大履修数、成績未入力の扱い等）の指摘

採点観点

• dom/ran の読み解きが正しい
• 制約が何を防ぐか説明できる

基礎理解演習2：操作スキーマの作成

ヒント（段階）

1. 正常系は Δ State と pre/post を分ける
2. エラー系は状態不変（Ξ State）とし、エラー原因を出力で示す

模範解答（骨子）

• 正常：存在確認＋未登録確認→enrollment更新
• エラー：学生不存在/科目不存在/重複履修の各スキーマ
• 統合：スキーマ和（正常 ⫿ エラー）で定義

採点観点

• 正常/エラーが分離されている
• 状態更新の影響が追跡できる

実践演習1：銀行システムのモデル化

ヒント（段階）

1. 顧客/口座/取引を集合と関係で表し、一意性/参照整合を不変に置く
2. 送金は「引き出し+預金」として合成可能な形にする

模範解答（骨子）

• 状態：accounts, owners, balance, txs など
• 不変：残高非負、口座番号一意、所有者存在、取引参照整合
• 操作：開設/預金/引出/送金（事前/事後/エラー）

採点観点

• 不変が制約と対応
• 操作が不変を保存する

実践演習2：スキーマ演算の活用

ヒント（段階）

1. 認証チェックを共通スキーマとして定義し、各操作に合成する
2. 正常/エラー統合は「結果の型（成功/失敗）」を揃える
3. 原子性は「途中失敗時に状態が戻る」ことを仕様で表現する

模範解答（骨子）

• Auth / Log スキーマを作り、操作と合成
• エラーを ErrorCode として統一
• 送金を合成し、失敗時は Ξ State を保証

採点観点

• 演算の使い所が合理的
• 例外時の状態が定義されている

発展演習：実時間システムの仕様化

ヒント（段階）

1. 時刻/タイマーは状態変数として明示する
2. 安全性（同時青禁止）を不変として固定し、活性/公平性を別枠で定義する

模範解答（骨子）

• 信号状態、センサー、歩行者要求、タイマーの状態スキーマ
• 遷移（信号変更）操作スキーマ
• 性質（安全/活性/公平）を検証可能な形で列挙

採点観点

• 安全性が不変で表現されている
• 時間制約が仕様に反映されている

D.7 第6章

基礎理解演習1：CSP記法の読解

ヒント（段階）

1. プロセス/チャネル/合成（並列/選択）の意味を説明する
2. 受送信の同期（ハンドシェイク）を前提に振る舞いを追う

模範解答（骨子）

• プロセス定義の逐次解釈
• 合成時の同期点と、可能なトレースの例

採点観点

• 記法の意味が正しく説明できる
• 具体トレースで説明できる

基礎理解演習2：デッドロック分析

ヒント（段階）

1. 相互待ちの原因は「双方が受信待ち/送信待ち」になる点
2. 回避策は順序合意/非同期化/タイムアウトなど。ただし副作用も述べる

模範解答（骨子）

• 最小デッドロック例（2プロセス、逆順の送受）
• 回避策と副作用（順序逆転、無限バッファ、遅延）

採点観点

• デッドロック状態が説明できる
• 回避策が現実的で、副作用も言及

実践演習1：ATMシステムの設計

ヒント（段階）

1. ATM/BankServer/User をプロセスとして分け、チャネルで接続する
2. 安全性（残高非負、二重引落なし）と活性（最終応答）を整理する

模範解答（骨子）

• プロセス分解と主要チャネル
• 失敗系（タイムアウト/再試行/中断）の扱い

採点観点

• プロトコルの順序制約が明確
• 失敗系の考慮がある

実践演習2：プロセス合成の活用

ヒント（段階）

1. 合成は「仕様側で許す振る舞い」を増やし過ぎないように注意
2. 合成後の性質（デッドロック不在、到達性）を確認する

模範解答（骨子）

• 合成手順と、合成後に成立させたい性質
• 検証結果の要約

採点観点

• 合成の意図が説明できる
• 合成での副作用が把握されている

発展演習：分散システムの設計

ヒント（段階）

1. 通信の非同期/遅延/損失を仮定し、前提を明記する
2. 失敗検知・再送・冪等性（idempotence）を設計に含める

模範解答（骨子）

• 障害モデルとプロトコル骨子
• 安全性/活性の性質定義

採点観点

• 障害モデルが明示されている
• 設計が性質と接続している

D.8 第7章

基礎理解演習1：時相論理の記法理解

ヒント（段階）

1. []（常に）と <>（いつか）を、要求の文に対応付ける
2. 公正性（WF/SF）は「いつか進む」の前提条件として分離する

模範解答（骨子）

• 各性質を []P / <>Q / P => <>Q 等へ変換
• 公正性仮定の候補

採点観点

• 安全/活性が混同されていない
• 公正性が前提として明示されている

基礎理解演習2：状態と行動の記述

ヒント（段階）

1. 変数（状態）とアクション（遷移）を分けて書く
2. Init と Next を定義し、Spec == Init /\ [][Next]_vars にまとめる

模範解答（骨子）

• 状態変数の定義
• Init/Next/Invariant の雛形

採点観点

• 記述がTLA+の基本形に沿っている
• 変数更新が一貫している

実践演習1：相互排除プロトコルの設計

ヒント（段階）

1. クリティカル区間の定義と、排他不変 ~(crit[0] /\ crit[1])
2. 活性を入れる場合は公正性仮定の過不足を点検する

模範解答（骨子）

• 状態（flag/turn等）とNext
• 不変（排他）と、必要なら活性（最終的に入れる）

採点観点

• 不変が破れない
• 公正性の扱いが妥当

実践演習2：生産者・消費者問題

ヒント（段階）

1. バッファ（有界/無界）と背圧の前提を明示する
2. 安全性（範囲外アクセス/オーバーフロー）と活性（進行）を分離する

模範解答（骨子）

• バッファ状態と操作（produce/consume）
• 不変：0 <= count <= N 等

採点観点

• 安全/活性が切り分けられている
• 有界性の前提が明示されている

発展演習：分散システムの設計

ヒント（段階）

1. メッセージ遅延/損失/重複の前提を明記する
2. 再送/ACK/タイムアウトの停止条件と冪等性を設計する

模範解答（骨子）

• 障害モデルとプロトコル
• 安全性（重複処理なし等）と活性（いつか到達）の定義

採点観点

• 前提と性質が整合している
• 再送戦略が停止条件まで含む

D.9 第8章

基礎理解演習1：時相論理の実践

ヒント（段階）

1. 「状態」と「イベント」を命題に落とし、LTL/CTLの構文へ写像する
2. 公平性や効率性は、前提と性質を分けて記述する

模範解答（骨子）

• 安全：AG(door_open -> AX ~moving)（CTL例）/ [](door_open => ~moving)（LTL例）
• 活性：AG(call -> AF arrive)（CTL例）/ [](call => <>arrive)（LTL例）

採点観点

• CTL/LTLの使い分けが妥当
• 命題化（状態/イベント）が一貫

基礎理解演習2：状態空間分析

ヒント（段階）

1. カウンタ値×各プロセスの局所状態で状態数を概算する
2. 競合は read-modify-write の分割で起こる

模範解答（骨子）

• 状態数の概算（値0-10＋局所状態）
• 競合例（lost update）
• 部分順序簡約が効く条件（独立な遷移の交換可能性）

採点観点

• 状態数の数え方が説明できる
• 競合の原因が具体

実践演習1：SPIN による検証

ヒント（段階）

1. Promelaでプロセス（reader/writer）と共有資源を定義する
2. 安全性（同時書込なし等）を assert や LTL で表す
3. 検証実行では seed/探索上限/反例を保存する

模範解答（骨子）

• モデル（promela）と性質（assert/LTL）
• 実行ログと反例（発生時）の要約

採点観点

• 性質が要求と対応
• 反例が再現可能

実践演習2：NuSMV による検証

ヒント（段階）

1. 状態変数（信号状態/センサー/要求）を定義する
2. 安全性はCTL/LTLで不変として書く（同時青禁止等）

模範解答（骨子）

• NuSMVモデルと性質
• 検証結果の要約（反例があればトレース）

採点観点

• 安全/活性/応答が分離
• 反例の解釈が妥当

発展演習：複数ツールによる段階的検証

ヒント（段階）

1. Phaseごとに抽象度と目的（何を潰すか）を明確にする
2. 反例は「抽象化の穴」か「設計欠陥」かを分類する

模範解答（骨子）

• Phase 1-3 の成果物（仕様/モデル/実装）と発見問題の分類
• ツール間の結果整合の確認

採点観点

• 抽象化レベルと発見問題の関係が説明できる
• 成果物が再現可能

D.10 第9章

基礎理解演習1：論理推論の形式化

ヒント（段階）

1. 命題を記号化し、自然演繹規則（導入/除去）に対応付ける
2. 推論2は「前提が現実の知識と衝突」する例（例外の扱い）として整理する

模範解答（骨子）

• 推論木（規則適用順）と妥当性評価
• 推論2の問題点：前提 ∀鳥. 飛べる が現実に対して過強

採点観点

• 形式化が正しい
• 問題点が「前提の誤り」として説明できる

基礎理解演習2：Rocq（旧称Coq）での基本証明

ヒント（段階）

1. intros → split/left/right → destruct/apply の基本流れ
2. 量化は intros x で取り、exists は exists x で構成する

模範解答（骨子）

• 証明戦略（タクティクス列）の提示
• 必要なら補助補題（forall の分配等）を先に定義

採点観点

• 証明が通る
• 戦略が説明できる（なぜそのタクティクスか）

実践演習1：データ構造の証明

ヒント（段階）

1. append/reverseは構造帰納法（induction l1 等）が基本
2. 先に length_append 等の補助補題を揃える

模範解答（骨子）

• append_assoc：l1に帰納、simpl と rewrite を用いる
• reverse_involutive：reverse_append を補助に使う

採点観点

• 補助補題の選定が妥当
• 証明が可読（過度な自動化に依存しない）

実践演習2：アルゴリズムの正しさ証明

ヒント（段階）

1. sortedの保存（insert_sorted）→ 全体のsorted（insertion_sort_sorted）の順で証明する
2. 正しさは「整列性」と「順列性」を分離する

模範解答（骨子）

• insert_sorted の証明骨子
• insertion_sort_permutation の証明骨子（Permutation補題の利用）

採点観点

• 性質分割ができている
• 証明が破綻せず通る

発展演習：実用的検証プロジェクト

ヒント（段階）

1. 対象を小さく切り、証明すべき性質（可逆性、不変保存等）を固定する
2. 実装より先に仕様（Prop）を定義し、証明が通る形へ調整する

模範解答（骨子）

• 選択したオプションと、仕様・不変・証明計画
• 発見した前提（境界条件、データ型制約）の整理

採点観点

• スコープが適切
• 実用上の示唆（何がコピー可能か）がある

D.11 第10章

基礎理解演習1：Hoare論理の基本

ヒント（段階）

1. 代入は代入公理（事後条件への代入）で逆算する
2. 条件分岐は分岐ごとの三項組を作り、合成する
3. ループは不変条件を置き、初期化/保持/終了で示す

模範解答（骨子）

• 課題1-1：{True} x:=y+2; z:=x*3 {z=3*(y+2)}（中間条件を含めてもよい）
• 課題1-2：分岐で result=|x| を意識
• 課題1-3：不変 sum = (i-1)*i/2 等を置く

採点観点

• 不変が正しく、推論が成立
• 事前条件が過強/過弱でない

基礎理解演習2：ループ不変条件の発見

ヒント（段階）

1. 「処理済み範囲」に対する性質を不変にする
2. 停止性は変位関数（残り要素数等）で示す

模範解答（骨子）

• 線形探索：i 未満にtargetがない/ある場合の関係
• 最大値探索：max は array[0..i-1] の最大
• 挿入ソート：外側ループで 0..i-1 が整列済み

採点観点

• 不変が初期化/保持/終了を満たす
• 変位関数が妥当

実践演習1：配列操作の検証

ヒント（段階）

1. 仕様（事前/事後）を最初に固定する（ソートなら順序＋順列）
2. 境界条件（配列範囲）を不変と同等に扱う

模範解答（骨子）

• 選んだアルゴリズムの仕様（正しさ・停止性）
• 主要不変と証明手順（骨子）

採点観点

• 性質分割（正しさ/停止性/安全）ができている
• 証明が追える

実践演習2：ツールを用いた検証

ヒント（段階）

1. Dafny等では requires/ensures/invariant を先に書く
2. 検証に通らない場合は、不変の弱さ/不足を疑う

模範解答（骨子）

• 実装コード（仕様注釈付き）
• 検証実行ログ
• つまずきと修正（不変強化、境界条件）

採点観点

• 機械検証が通っている
• 失敗時の修正が説明できる

発展演習：実用的システムの部分検証

ヒント（段階）

1. 対象範囲を限定し、性質を3つ程度に絞る
2. 仕様→テスト/CIへの統合まで書けると実務価値が上がる

模範解答（骨子）

• 対象選定理由
• 性質、仕様、検証アプローチ
• 発見問題と改善提案

採点観点

• スコープと性質が妥当
• 実用化の課題が言語化されている

D.12 第11章

理解確認演習1：導入戦略の評価

ヒント（段階）

1. 段階導入（小さく始める）に反していないかを確認する
2. KPIは「再現率」「MTTR」「重大障害の減少」等に落とす

模範解答（骨子）

• 計画の問題点（過大/全社一律/短期評価）
• 段階導入案（パイロット→拡散）とKPI

採点観点

• 現実的な計画に修正できている
• KPIが測定可能

理解確認演習2：組織文化分析

ヒント（段階）

1. 技術課題と文化課題を分ける
2. 抵抗の原因を「負担増」「評価不安」「スキル差」などに分解する

模範解答（骨子）

• 現状文化の特徴
• 障害要因/促進要因
• 変革戦略（教育、標準化、成功体験）

採点観点

• 分析が具体
• 施策が実行可能

実践演習1：ROI分析

ヒント（段階）

1. バグ修正コスト差分（上流で潰す効果）をベースに試算する
2. 前提は必ず明示し、感度分析（±）を入れる

模範解答（骨子）

• 前提と算式
• 導入コストと削減効果の比較
• 不確実性（前提依存）とリスク

採点観点

• 計算根拠が追える
• 前提の妥当性が説明できる

実践演習2：プロセス統合設計

ヒント（段階）

1. PR/夜間/リリース前の段階化（図11-1）で配置する
2. 失敗時のartifact保存と再現手順を必須にする

模範解答（骨子）

• ゲート設計（強制/ソフト）
• 例外フロー（承認者、期限、ロールバック）

採点観点

• 再現性と運用が担保されている
• 例外が常態化しない設計

発展演習：包括的導入計画

ヒント（段階）

1. 人材・プロセス・ツールの3軸でロードマップ化する
2. 失敗パターン（過大導入、ツール分断）を先に潰す

模範解答（骨子）

• 1年計画（段階、成果物、教育）
• 合意形成とガバナンス

採点観点

• 実行計画が段階的
• ガバナンスが明確

D.13 第12章

理解確認演習1：ツール選択マトリクス

ヒント（段階）

1. 問題領域（安全クリティカル、並行、分散）と手法の適合を整理
2. 学習/運用コスト、CI統合の容易さを評価軸に含める

模範解答（骨子）

• ツール候補と選定理由（要件/制約/リスク）
• 18ヶ月の段階計画（導入→定着）

採点観点

• 評価軸が明確
• 計画が現実的

理解確認演習2：CI/CD統合設計

ヒント（段階）

1. PRの最小検証は「短い・安定・再現可能」に寄せる
2. 夜間で偽陰性を下げ、リリース前でクリティカル性質を確定する

模範解答（骨子）

• PR/夜間/リリース前のジョブ構成
• artifact保存と例外承認

採点観点

• 段階化が妥当
• 反例の運用が設計されている

実践演習1：コード生成戦略

ヒント（段階）

1. 生成物は「未信頼」として扱い、検証器で閉じる
2. 仕様差分と実装差分を同期させる

模範解答（骨子）

• 生成対象（仕様/テスト/契約）とレビュー観点
• 検証とCIゲートの設計

採点観点

• 信用境界が明確
• 再現性が確保されている

実践演習2：ツール導入失敗の事例分析

ヒント（段階）

1. 失敗要因を「技術」「プロセス」「組織」で分類する
2. 再発防止はチェックリスト化する

模範解答（骨子）

• 失敗要因の分類
• 改善策（段階導入、テンプレ、CI統合）

採点観点

• 原因分析が具体
• 改善策が運用に落ちている

発展演習：統合ツールチェーン設計

ヒント（段階）

1. ツール間の成果物（仕様/ログ/反例）を共通フォーマットで管理する
2. キャッシュ/バージョン固定で再現性を担保する

模範解答（骨子）

• ツールチェーン構成図
• 依存固定、artifact、例外フロー

採点観点

• 再現可能性が説明できる
• 運用コストが現実的

D.14 第13章

理解確認演習1：事例比較分析

ヒント（段階）

1. 技術/組織/経済/外部要因で比較表に落とす
2. 「コピー可能な教訓」と「固有事情」を分離する

模範解答（骨子）

• 比較表
• 共通成功要因と差異
• 適用判断の観点

採点観点

• 比較軸が体系的
• 教訓が一般化されている

理解確認演習2：業界適用可能性分析

ヒント（段階）

1. 規制/安全要求/障害モデルが強い業界ほど適用価値が高い
2. まず「小さく検証できる領域」から入る

模範解答（骨子）

• 対象業界のリスクと、適用候補領域
• 導入ステップとKPI

採点観点

• 業界特性が反映されている
• 導入が段階的

実践演習1：事例詳細調査

ヒント（段階）

1. 一次・準一次情報を最低3件参照し、主張に出典を付与する
2. 何を保証したか（性質）と、どう再現できるか（最小セット）を書く

模範解答（骨子）

• 出典リスト
• 性質と再現手順の要約

採点観点

• 出典が適切
• 再現可能性が示されている

実践演習2：導入計画策定

ヒント（段階）

1. 重要性（クリティカル度）で対象を選別する
2. CI統合と例外フローを計画に含める

模範解答（骨子）

• 対象選定、検証手法、段階導入、KPI

採点観点

• 計画が現実的
• ガードレールがある

発展演習：未来シナリオ分析

ヒント（段階）

1. 技術進歩（AI/検証自動化）と規制強化を前提にシナリオを複数作る
2. 不確実性は仮説として分離し、根拠（出典/前提）を併記する

模範解答（骨子）

• シナリオ2-3本と、前提・影響・対応策

採点観点

• 仮説と事実が分離
• 示唆が実務に落ちる

D.15 AI利用時の提出テンプレ（共通）

AIの出力は「提案」として扱い、合否は検証器で判定します。提出物は以下を満たしてください。

• 使用したプロンプト（要件/制約を含む）
• 生成された仕様・不変条件
• 検証コマンドとログ（seed/深さ/スコープ/所要時間）
• 反例が出た場合の修正履歴（差分と再検証ログ）

提出フォーマット（例）:

## 使用プロンプト
...

## 生成された仕様
...

## 検証ログ
command: ...
seed: ...
depth/scope: ...
result: ...

## 反例と修正
counterexample: ...
fix: ...
recheck: ...