4

私は Microsoft DevLabs Code Contracts 静的アナライザーを採用しようとしましたが、それが自分なのかそれとも彼らなのか実際にはわからない状況に直面しました。コードは次のとおりです。

    public static int GenerateInBetween(int min, int max)
    {
        Contract.Requires(min < max);
        Contract.Requires((long)(max - min) <= (long)(Int32.MaxValue));

        Contract.Ensures(Contract.Result<int>() >= min);
        Contract.Ensures(Contract.Result<int>() <= max);  // Unpvoven!

        long range = max - min;

        double basicRandom = new Random().NextDouble();
        Contract.Assert(basicRandom >= 0.0);
        Contract.Assert(basicRandom <= 1.0);              // Unpvoven!

        double randomDouble = basicRandom * range;
        Contract.Assert(randomDouble >= 0.0);
        Contract.Assert(randomDouble <= (double)range);   // Unpvoven!

        int randomInt32 = (int)randomDouble;
        Contract.Assert(randomInt32 >= 0);
        Contract.Assert(randomInt32 <= range);

        return min + randomInt32;
    }

静的アナライザーは、コメントされた事後条件とアサートを証明できなかったと主張します。いつそれが間違っているのかわかりませんでした。

編集asserts を asserts に置き換えても、事後条件はまだ証明されていません。

4

2 に答える 2

1

さて、最初は2つに分けられると思いましたが、最初の答えは実際には実際の問題に答えていないことに気づきました。

問題の最短バージョンは次のとおりです。

    public static void GenerateInBetween(double min, double max)
    {
        Contract.Requires(min < max);
        double range =  max - min;

        double randomDouble = 1.0 * range;
        Contract.Assert(randomDouble <= range);   
    }

別のコメント提供者が述べたように、ハードコードされた1.0を値<= 0.5に変更すると、チェックに合格します。0.5より大きい場合、失敗します。

ただし、Contract.Requires（min <max）行を削除すると、常に失敗します。

現時点では説明がありません。申し訳ありません。

于 2009-10-31T14:45:59.673 に答える
0

私はあなたの例を試し、それを最も基本的な例に要約しようとしました.

いくつかの問題があるようですが、ここに 1 つの大きな問題を示すと思われる例を示します。

public static void TestMethod()
{
    double d = MethodReturningDouble();
    Contract.Assert(d >= 0.0);
    Contract.Assert(d <= 4.0);
}

public static double MethodReturningDouble()
{
  //  Contract.Ensures(Contract.Result<double>() <= 4.0); // <- without this line the above asserts are unproven
    return 3.0;
}

呼び出されたメソッドのコード コントラクト仕様がないと、静的チェッカー/アナライザーは他に何も解決できないようです。MethodReturningDouble() は定数を返しますが、静的チェッカーはアサートが常にパスすることをうまく処理できません。

結論として、静的アナライザーはコードコントラクト仕様専用であり、一般的な分析用ではないようです。

呼び出すメソッド (コントラクトが定義されていない) に関する仮定を追加することができます。

例えば：

public static void TestMethodUsingRandom()
{
    double d = new Random().NextDouble();
    Contract.Assume(d <= 1.0);

    Contract.Assert(d >= 0.0);
    Contract.Assert(d <= 4.0);
}

特定のメソッドが特定の方法で動作することが確実にわかっている場合、これは正当な行為です。

于 2009-10-31T13:08:35.313 に答える