ソフトウェア工学 静的検証
プログラムの静的検証（static V&V of program）
検証とは、仕様の検証を行うもので、動的解析と静的解析がある。
静的検証は、正当性の証明を行う。動的検証では、プログラムが完全に正しいことは保証的ない。
正当性証明の手順
①仕様を事前条件と事後条件で記述
②ループに対して不変表明をおく．その他の表明を必要に応じて挿入
③事前条件／事後条件や表明を前後に持つプログラムの実行経路について，経路の先頭
の条件から，最後の条件が導き出されることを証明
– 例：Hoare論理の利用
④プログラムが正しく停止することを証明
Hoare論理
手続き型言語の要素に対して形式的意味を定義する。
すべての原穂は以下4つで表現できると仮定し、表記を置き換えていく。
① 代入文： x := e
代入文の公理（割当公理） {Q[e/x]} x := e {Q}
代入文x := e の実行後に事後条件Qが成り立つためには，事前条件としてQ[e/x]が成り
立っている必要がある
例 – {x+1 = 10} x := x+1 {x = 10}
② if文の規則： if B then S1 else S2 end
（ELSEあり）{P and B} S1 {Q} {P and not B} S2 {Q} / {P} if B then S1 else S2 end {Q}
（ELSEなし）{P and B} S {Q} P and not B ⇒ Q / {P} if B then S end {Q}
③while文の規則： while B do S end
{P and B} S {P} / {P} while B do S end {P and not B}
ループで何もしなくて出てくる場合もあるので、ループ前でも成立するPが肝になる。
④ 複合文： S1; …; Sn
複合文の規則（連結規則）{P} S1 {R1} {R1} S2 {R2} ... {Rn-1} Sn {Q}/{P} S1; S2; ... ; Sn {Q}
⓹帰結の規則
P⇒P1 {P1} S {Q1} Q1⇒Q / {P} S {Q}
※P1の条件をいかに弱い条件にできるかが重要。ー最弱事前条件
※簡単なIF文でも人手でやるのでとても時間がかかる
制御フロー・データフロー解析（control flow/data flow analysis）
・プログラム要素間の依存関係の解析
– 制御的な依存関係
– データの依存関係
・制御フローグラフ
– 制御の依存関係を図示
・データフローグラフ
– データの依存関係を図示
・依存関係の把握
– 変更が影響する範囲の特定
– 誤りの場所や原因の特定
プログラムスライシング（program slicing）
特定の文や変数値に関係するプログラムの部分を抽出したもの。プログラム依存グラフ（PDG）の作成を行う。
コードクローン分析（code clone analysis）
コードクローンとはソースコード中に存在する，全く同一あるいは類似したコード断片のこと。コードクローンは単なるコピー&ペーストによって発生したり、 常套句的なプログラム記述であったり（ 例：ファイルのオープン，データベース接続など）、何らかの意図に基づくなどの理由で発生する。
コードクローンの弊害はソフトウェアの保守が難しくなること。そのため、検証の立場からするとクローンを除去することが重要になる。ーリファクタリングという。
クローンを自動的に見つけようとすると、コードクローンの定義が必要になるが、定義を決めるのは困難。
●コードクローンの検出方法
– 行単位の比較に基づく方法
検出の精度は低いので実用的ではない。：'{', '}' の位置やそれらの有無による違いによっても検出が不可になる。
– 抽象構文木の比較に基づく方法
ソースコードの構文解析結果から抽象構文木（AST: Abstract Syntax Tree)を作成。コンパイラ技術の延長で、商用のツールも存在する。（CloneDR)
– プログラム依存グラフの比較に基づく方法
ソースコードの意味解析結果からプログラム依存グラフ（PDG）を作成
– メトリクスに基づく方法。検出の精度は高いが計算量が膨大。
関数・メソッドの部品単位でメトリクスを計算しメトリクスの値が近いものをコードクローンとして抽出する。
– トークンの比較に基づく方法
ソースコードに出現するトークンの系列を比較し，類似するサブ系列をコードクローンとして検出。適切な精度を保ちながら，大規模なコードの解析にも利用可能。
