2

次のようなコードがあります。

     if conditionA(x, y, z) then doA()
else if conditionB(x, y, z) then doB()
...
else if conditionZ(x, y, z) then doZ()
else throw ShouldNeverHappenException

(静的分析を使用して) 2 つのことを検証したいと思います。

  1. すべての条件conditionA, conditionB, ..., conditionZが相互に排他的である場合 (つまり、2 つ以上の条件が同時に真になることはあり得ない)。
  2. 考えられるすべてのケースがカバーされます。つまり、「else throw」ステートメントは呼び出されません。

これを（簡単に）実行できるツールや方法を教えてください。

「Prolog を使用する」または「Mathematica を使用する」よりも詳細な情報をいただければ幸いです... ;-)

アップデート：

conditionA, conditionB, ..., conditionZが (純粋な) 関数であり、x、y、z が「プリミティブ」型であると仮定します。

4

4 に答える 4

2

あなたがしたい項目1.は文体の問題です。条件が排他的でなくても、プログラムは理にかなっています。個人的には、静的分析ツールの作成者として、ユーザーはスタイルを強制しようとせずに十分な誤報を受け取ると思います (別のプログラマーは意図的に重複する条件を書くので、そのプログラマーにあなたが尋ねることは誤報になるでしょう) . つまり、構成可能なツールがあります。そのうちの 1 つについては、この構造が検出されたときにケースが排他的でなければならないというルールを作成できます。また、Jeffrey が提案したように、オーバーラップがない場合に true であるブール条件を計算するコンテキストでコードをラップし、代わりにその条件をチェックすることができます。

項目 2. はスタイルの問題ではありません。例外が発生する可能性があるかどうかを知りたいのです。

この問題は理論上も実際上も困難であるため、ツールは通常、正確性(問題がある場合に必ず警告する) または完全性 (問題がない場合に警告することはない)の少なくとも 1 つを放棄します。変数の型が無制限の整数である場合、計算可能性理論は、アナライザーが正確かつ完全であることはできず、すべての入力プログラムに対して終了すると述べます。しかし、理論で十分です。一部のツールは正確性と完全性の両方を放棄しますが、それはそれらが役に立たないという意味ではありません。

正しいツールの例はFrama-Cの値分析です: ステートメント (一連の elseifs の最後のケースなど) が到達不能であると示されている場合、到達不能であることがわかります。完全ではないため、最後のステートメントに到達できないと言わなければわかりません。

完全なツールの例はCuteです。これはいわゆるコンコリックアプローチを使用してテスト ケースを自動的に生成し、構造的なカバレッジを目指します (つまり、多かれ少なかれヒューリスティックに、最後のケースをすべて一度アクティブ化するテストを生成しようとします)。他は撮影済み）。テストケース (コードが実際に実行される単一の明確な入力ベクトル) を生成するため、問題がないことを警告することはありません。これが完全であるということです。しかし、最後のステートメントが存在する場合でも、最後のステートメントに到達する原因となるテスト ケースを見つけることができない場合があります。それは正しくありません。

于 2010-04-21T20:40:29.253 に答える
1

条件がブール値の述語 X、Y、Z に対するブール式 (and/or/not) であると仮定すると、質問はシンボリックブール評価エンジンで簡単に解決されます。

それらがすべてのケースをカバーしているかどうかについての質問は、すべての条件の選言を取り、トートロジーであるかどうかを尋ねることによって答えられます。Wang のアルゴリズムはこれをうまく処理します。

それらが交差するかどうかについての質問は、ペアごとに答えられます。式 a と b に対して、a & b == false をシンボリックに構成し、Wang のトートロジー テストを再度適用します。

DMS Software Reengineering Toolkitを使用して、C のプリプロセッサ条件に対して同様のブール値計算 (部分評価) を実行しました。DMS は、ソース コードを解析する機能を提供します (大規模なコード ベースおよび/または時間の経過とともにプログラムを変更するときに繰り返し)、プログラムの断片を抽出し、それらを記号的に構成してから、書き換え規則を適用します (ブールの単純化または Wang のようなアルゴリズムを実行するため)。

于 2010-04-22T07:40:11.120 に答える
1

これは、NP 困難な 3-sat 方程式を解くのと同型のようです。残念ながら、静的アナライザーがこのドメインをカバーしようとする可能性は低いです。

于 2010-04-21T19:25:11.243 に答える
1

一般的なケースでは、これは — @Michael Donohue が指摘しているように — NP 困難な問題です。

しかし、チェックする条件が妥当な数しかない場合は、それらすべてをチェックするプログラムを作成できます。

for (int x = lowestX; x <= highestX; x++)
    for (int y ...)
      for (int z ...)
      {
          int conditionsMet = 0;
          if conditionA(x, y, z) then conditionsMet++;
          if conditionB(x, y, z) then  conditionsMet++;
          ... 
          if conditionZ(x, y, z) then  conditionsMet++;
          if (conditionsMet != 1)
              PrintInBlinkingRed("Found an exception!", x, y, z)
      }
于 2010-04-21T19:33:11.600 に答える