第9章 形式手法

9.1 形式手法とは

9.1.1 硬いソフトウェア

バグが許されない場合もある

P.148下～

厳密な記述/検証

9.1.2 形式的仕様記述

モデル規範型

モデルを記述

性質規範型

性質を記述

プロセス代数

対象は通信

9.1.3 形式検証

プログラム検証

フロイド-ホーア論理（後出）

システム検証

時相論理式： 時間進行により命題の真偽が変化

P.151中～

□： いつでも
◇： いつかは

P.151下～

省略

9.1.4 抽象化と軽量形式手法

省略

確認問題 第9章a

9.2 フロイド-ホーア論理によるプログラム検証

9.2.1 フロイド-ホーア論理

事前条件と事後条件で仕様を表現する

部分的正当性と完全正当性

P:事前条件
S:プログラム
Q:事後条件

{P}S{Q} （停止するならQ）

P.154下～

[P]S[Q] （停止してQ）

P.155上～

証明体系

(A1)空文の公理

(A2)代入文の公理

{x=1[1/x]}x:=1{x=1}

(R1)

(R2)

(R3)

(R4)

証明例

プログラムを実行したら総和が求まることの証明

9.2.2 プログラムの停止性

省略

確認問題 第9章b

レポート9

教科書（図はすべてこちらより引用）：
　鵜林尚靖,「レクチャー ソフトウェア工学」, 数理工学社