35

( MSDN フォーラムにも投稿されていますが、私が見る限り、トラフィックはそれほど多くありません。)

Assertとの例を提供しようとしていますAssume。これが私が持っているコードです:

public static int RollDice(Random rng)
{
    Contract.Ensures(Contract.Result<int>() >= 2 &&
                     Contract.Result<int>() <= 12);

    if (rng == null)
    {
        rng = new Random();
    }
    Contract.Assert(rng != null);

    int firstRoll = rng.Next(1, 7);
    Contract.Assume(firstRoll >= 1 && firstRoll <= 6);

    int secondRoll = rng.Next(1, 7);
    Contract.Assume(secondRoll >= 1 && secondRoll <= 6);

    return firstRoll + secondRoll;
}

(もちろん、既存の参照の代わりに null 参照を渡すことができるというビジネスRandomは、純粋に教育的なものです。)

firstRollチェッカーがそれを知っていて、secondRollそれぞれが範囲内[1, 6]にある場合、合計が範囲内にあると判断できると思っていました[2, 12]。

これは無茶な希望ですか？何が起こるかを正確に把握するのはトリッキーなビジネスだと思います...しかし、チェッカーが十分にスマートであることを望んでいました:)

これが現在サポートされていない場合、近い将来サポートされる可能性があるかどうかを知っている人はいますか?

編集:静的チェッカーの算術演算には非常に複雑なオプションがあることがわかりました。「高度な」テキスト ボックスを使用して、Visual Studio からそれらを試すことができますが、私が知る限り、それらが何をするかについての適切な説明はありません。

4

2 に答える 2

14

MSDN フォーラムに回答がありました。私はすぐそこにいたことがわかりました。基本的に、「and-ed」コントラクトを分割すると、静的チェッカーはより適切に機能します。したがって、コードを次のように変更すると:

public static int RollDice(Random rng)
{
    Contract.Ensures(Contract.Result<int>() >= 2);
    Contract.Ensures(Contract.Result<int>() <= 12);

    if (rng == null)
    {
        rng = new Random();
    }
    Contract.Assert(rng != null);

    int firstRoll = rng.Next(1, 7);
    Contract.Assume(firstRoll >= 1);
    Contract.Assume(firstRoll <= 6);
    int secondRoll = rng.Next(1, 7);
    Contract.Assume(secondRoll >= 1);
    Contract.Assume(secondRoll <= 6);

    return firstRoll + secondRoll;
}

それは問題なく動作します。また、この例は、コントラクトを分離した方がチェッカーがうまく機能するというまさにその点を強調しているため、この例がさらに有用であることも意味します。

于 2009-08-07T20:27:26.673 に答える
1

MS Contracts Checker ツールについては知りませんが、範囲分析は標準的な静的分析手法です。商用の静的分析ツールで、添字式が有効であることを確認するために広く使用されています。

MS Research はこの種の静的分析で優れた実績を持っているため、現在チェックされていなくても、このような範囲分析を行うことが契約チェッカーの目標になると期待しています。

于 2009-08-07T14:10:46.743 に答える