不完全なテスト対網羅的な分析対リンゴとオレンジの比較はどちらですか？

Question

私はよくこのような議論を聞いています。従来のテストの欠点は、合金分析が完全で（境界内で）完全であるのに対して、不完全であるということです。しかし、最初はソフトウェアについて話しており、2番目はモデルについて話しています。それはリンゴとオレンジの比較ではありませんか？

更新：私は間違っていました。比較はこれではありません：testing code versus analyzing models。これはリンゴとオレンジの比較です。代わりに、比較は次のとおりです。

Testing models versus analysis of models. 

Testing code versus analysis of code. 

これはリンゴとリンゴの比較です。

したがって、アーティファクトがモデルであろうとコードであろうと、2つの種類の分析を比較することができます。テストは、サイズに制限のない比較的少数のケースをランダムに描画することに対応します。小規模な範囲内のすべてのケースを含む。

私の誤解を解消したDaniel Jacksonに感謝します。

Answer 1

最初に、合金が発明されたとき、実証ベースのシナリオを使用してモデルをテストするZやVDMなどのデータ豊富な言語のモデルを分析するための唯一のツールはありませんでした。各シナリオはユーザによって作成されたので、シナリオを作成するコストと少数の低いカバレッジの問題がありました。

第2に、Alloyがコード内のバグを見つけるために使用されました。Mandana Vaziri、Mana Taghdiri、Greg Dennis、Juan Pablo Galeottiなどの博士論文を参照してください。これらのすべてにおいて、従来のテストを回避したバグが発見されました。

第3に、限られた網羅的なテストが実行可能になっていることは注目に値する。 Sarfraz Khurshidは、当初はAlloyをベースにしたTestEraというツールでテストケースを作成し、後に（Darko Marinovらと共に）Koratと呼ばれるツールで、宣言的ではない制約。