c# - pex の制限に関する質問

Question

私はいくつかの c# コードでテストを実行していますが、pex は Math.Acos を含むステートメントをカバーしていませんでした (これは大きな switch ステートメントの一部です)。なぜpexにこの制限があるのか​​ 誰かが知っているかどうか知りたいですか? オンラインで調べましたが、何も見つかりませんでした。

Answer 1

Pexは、次にカバーしようとするパスの制約システム（パス条件）を構築します。次に、制約ソルバーに依存して、その制約システムの満足のいく割り当てを生成します。場合によっては、制約ソルバーが（妥当な時間内に）値を見つけることができません。現時点では、これは主に浮動小数点変数または10進型の変数を含むコードで発生します。

たとえば、Math.Acos（x）<=yの条件を満たす必要があるとします。Pexが前の実行（Math.Acos（x）> y）で入力xによってMath.Acos関数を通過したパスをトレースできない限り、制約ソルバーはそれを解決するためにMath.Acosがどのように機能するかを理解する必要があります。制約。

PexがMath.Acosの実装にアクセスできる場合でも、結果として得られる制約システムは複雑すぎて、制約ソルバーが妥当な時間内に処理できない可能性があります。