Polyspace 検証で近似が使用される理由
Polyspace® Code Prover™ では、"静的検証" を使用してランタイム エラーが発生しないことが証明されます。静的検証は、実際にプログラムを実行せずにプログラムの動的プロパティを引き出します。静的検証は、検証が特定のテスト ケースや一連のテスト ケースに依存しないため、実行時デバッグなどの他の手法とは大きく異なります。静的検証で得られるプロパティは、プログラムの "あらゆる" 実行に当てはまります。1 .
静的検証では、ソフトウェアの演算とデータの典型的な近似が使用されます。たとえば、以下のコードを考えます。
for (i=0 ; i<1000 ; ++i) {
tab[i] = foo(i);
}i が tab の範囲を超えていないことをチェックするアプローチの 1 つは、i が取り得るそれぞれの値を検討することです。このアプローチには 1,000 回のチェックが必要です。静的検証では、本ソフトウェアによって変数の領域別にその変数がモデル化されます。この場合、本ソフトウェアでは静的な間隔 [0..999] に属するものとして i がモデル化されます。本ソフトウェアでは、データの複雑さに応じて、凸多面体や整数格子など、さらに詳細なモデルがこの目的に使用されます。
近似は、その定義上、情報の喪失につながります。たとえば、検証では、ループの各サイクルで i が 1 ずつインクリメントされるという情報は失われます。ただし、この情報がない場合でも、i の範囲を tab の範囲より確実に小さくすることができます。このプロパティを確立するのに必要なチェックは 1 つのみです。したがって、静的検証は、従来のアプローチに比べて効率的です。
近似を行う際、検証では網羅性が妥協されません。その理由は、過大近似が行われるためです。言い換えれば、変数について計算される領域は、実際の領域のスーパーセットになります。
1 The properties obtained from static verification hold true only if you execute your program under the same conditions that you specified through the analysis options. For instance, the default verification assumes that pointers obtained from external sources are non-null. Unless you specify the option 環境ポインターが安全でないことを考慮する (-stubbed-pointers-are-unsafe), the verification results are obtained under this assumption. They might not hold true during program execution if the assumption is invalidated and a null pointer is obtained from an external source.
