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));

我认为您可能是对的：静态检查器还不能证明一切，并且还依赖于基类库。该线程中的人们似乎在谈论静态检查器如何由于一般可空类型的合同实现中的错误而无法正确理解可空类型。

当然你也可以这样写，解决你的问题：

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 回答