7.2. プログラムの検証

7.2.1 ソフトウェア・モデル検査

(1) 有界モデル検査の応用

省略

(2) 実行列の論理表現

代入文をSSA(Static Single Assignment)で表現する

P.176中～

代入文ごとに新しい変数を導入

→ それぞれの状態での変数の値を表現する

P.176下～

x2=x1 : 代入されなければ前の値のまま

P.177上～

C⇒P （このプログラムならこの命題が成り立つこと）を検査したい

→ ￢(C⇒P) を満たす解を探す

P.177中～

(3) 繰り返し文の取り扱い

while文を表すのにwhile文を用いており、解決にならない

P.178下～

繰り返し回数を定めれば論理式にできる

[ex13-1] x=y+1; if (x==0) then x=2; というプログラムをSSAで解釈するとxを表す変数はいくつ必要ですか

[ex13-2] C⇒Pであることを確認するために、代わりに￢(C⇒P)について確認するべきなのはどんな場合ですか

[ex13-3] SSAによる表現と相性が悪いのはどれですか

7.2.2 コントラクト

(1) モジュラー検証

Design by Contract

{事前条件}プログラム{事後条件}

P.179中～

呼び出し前状態 ⇒ {事前条件}

{事前条件}∧{事後条件} ⇒ 呼び出し後状態

P.179下～

Dikstraの最弱事前条件は省略

P.180中～

モジュラー検証で

• 計算量削減

• ソース無くても検証

P.180中～

事前条件にない情報が必要ななケースではNG

(2) 有界モデル検査とモジュラー検証

P.181上～

Pre ⇒ (C ⇒ Post)

P.181中～

P.181下～

P.182上～

ex2を呼び出す

P.182中～

P.182中～

インライン展開 → 論理式も増大

P.182下～

モジュラー検証(1/2):

呼び出し前状態 ⇒ {事前条件}

P.183上～

(2/2)

{事前条件}∧{事後条件} ⇒ assert

P.183下～

モジュラー検査でスケーラビリティの問題を回避

[ex13-4] モジュラー検査のメリットはどれですか

[ex13-5] インライン展開して検査をするメリットはどれですか

課題

教科書（図はすべてこちらより引用）：
　中島震，「形式手法入門―ロジックによるソフトウェア設計―」，オーム社