0

静的コントラクト チェック ツールでバグを見つけたと思います。全体を でタグ付けする以外に方法はあり[ContractVerification(false)]ますか?

class Employee
{
    public int? HierarchyLevel { get; private set; }

    public Employee(int? level)
    {
        Contract.Requires<ArgumentException>(
            (!level.HasValue) 
            || 
            level >= 0 && level <= 10);
        Contract.Ensures(
            (!HierarchyLevel.HasValue) 
            || 
            (HierarchyLevel.Value >= 0 && HierarchyLevel.Value <= 10));
        this.HierarchyLevel = level; //unproven

        // this doesnt work either
        //if (!level.HasValue) {
        //    this.HierarchyLevel = new Nullable<int>();
        //} else {
        //    this.HierarchyLevel = new Nullable<int>(level.Value);
        //}

        // can't even make the static checker shut up with that:
        //Contract.Assume(
        //    (!HierarchyLevel.HasValue) 
        //    || 
        //    (HierarchyLevel.Value >= 0 && HierarchyLevel.Value <= 10));
    }
}

驚いたことに、以下のバージョンが動作します。しかし、コントラクト検証ツールを喜ばせるためだけに、単一のコードを書き始めたり、独自のバージョンの Nullable を導入したりしたくはありません。

class Employee2
{
    public int HierarchyLevel { get; private set; }
    public bool HasLevel { get; private set; }
    public Employee2(int level, bool hasLevel)
    {
        Contract.Requires<ArgumentException>(!hasLevel || level >= 0 && level <=10);
        if (hasLevel) {
            HasLevel = true;
            HierarchyLevel = level;
        } else {
            HasLevel = false;
            HierarchyLevel = -1;
        }
    }
    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(
            (!HasLevel) || 
            (HierarchyLevel >= 0 && HierarchyLevel <= 10));
    }
}
4

1 に答える 1

1

まず第一に、あなたはあなたのコードでいくつかの中括弧を置き忘れました（しかしこれはあなたの問題を解決しません）：

Contract.Requires<ArgumentException>(!level.HasValue
    || (level.Value >= 0 && level.Value <= 10));
Contract.Ensures(!HierarchyLevel.HasValue
    || (HierarchyLevel.Value >= 0 && HierarchyLevel.Value <= 10));

あなたは正しいかもしれないと思います。静的チェッカーはまだすべてを証明することはできず、基本クラスライブラリにも依存しています。このスレッドの人々は、一般的なnull許容型のコントラクト実装のエラーのために、静的チェッカーがnull許容型を正しく理解できない方法について話しているようです。

もちろん、次のように書くこともできます。これで問題が解決します。

Contract.Requires<ArgumentException>(!level.HasValue
    || (level.Value >= 0 && level.Value <= 10);
Contract.Ensures(HierarchyLevel == level);

そして、ここにあなたの問題に対する別の解決策があります。条件を別のメソッドに入れ、メソッドにPureAttribute（メソッドに副作用がないことを示す）のマークを付けます。次に、次のように、入力引数と保証値の両方にメソッドを適用します。

[Pure]
public static bool IsInRange(int? value)
{
    return !value.HasValue
        || (value >= 0 && value <= 10);
}

public Employee(int? level)
{
    Contract.Requires<ArgumentException>(IsInRange(level));
    Contract.Ensures(IsInRange(HierarchyLevel));
    this.HierarchyLevel = level;
}
于 2012-07-27T10:32:26.137 に答える