c# - 代码契约(Contract)不能反转条件？

Question

我有这个结构(为简洁起见简化):

public struct Period
{
    public Period(DateTime? start, DateTime? end) : this()
    {
        if (end.HasValue && start.HasValue && end.Value < start.Value)
        {
            throw new ArgumentOutOfRangeException("end", "...");
        }
        Contract.EndContractBlock();

        this.start = start;
        this.end = end;
    }

    private readonly DateTime? start;
    private readonly DateTime? end;

    public static Period operator +(Period p, TimeSpan t)
    {
        Contract.Assume(!p.start.HasValue || !p.end.HasValue || p.start.Value <= p.end.Value);
        return new Period(
            p.start.HasValue ? p.start.Value + t : (DateTime?) null,
            p.end.HasValue ? p.end.Value + t : (DateTime?) null);
    }
}

但是静态检查器给了我这个警告:

CodeContracts: requires unproven: end.HasValue && start.HasValue && end.Value >= start.Value

它从自定义参数验证中推断出的这个要求完全是错误的。我想为 start 允许空值或 end ，并且只需要 start <= end如果两者都提供。但是，如果我将构造函数更改为:

public Period(DateTime? start, DateTime? end) : this()
{
    Contract.Requires(!start.HasValue || !end.HasValue || start.Value <= end.Value);
    this.start = start;
    this.end = end;
}

我收到了这个警告，看起来更正确，但很难看出为什么无法证明需求:

CodeContracts: requires unproven: !start.HasValue || !end.HasValue || start.Value <= end.Value

我以为 ?: 可能有问题，但是当我将运算符更改为:

public static Period operator +(Period p, TimeSpan t)
{
    var start = p.start.HasValue ? p.start.Value + t : (DateTime?) null;
    var end = p.end.HasValue ? p.end.Value + t : (DateTime?) null;

    Contract.Assume(!start.HasValue || !end.HasValue || start.Value <= end.Value);
    return new Period(start, end);
}

当然，如果我更改 .Requires至 .Assume ，警告完全消失，但这不是可接受的解决方案。

因此，代码契约(Contract)中的静态检查器似乎无法正确反转条件。而不是简单地通过用 !(…) 包装来反转条件或申请 De Morgan's law (如上所示)，它似乎只是反转条件的最后一个组件。使用自定义参数验证时，静态检查器是否无法正确解释复杂的条件？

有趣的是，我尝试了这个，认为静态检查器只会剥离 !在前面，但没有:

if (!(!start.HasValue || !end.HasValue || start.Value <= end.Value))
{
    throw new ArgumentOutOfRangeException("end", "...");
}
Contract.EndContractBlock();

CodeContracts: requires unproven: !(!(!start.HasValue || !end.HasValue || start.Value <= end.Value))

在这种情况下，它只是用 !(…) 包装了整个条件。 ，即使它没有必要。

另外，如果我更改可为空的 DateTime只是简单的不可为空 DateTime并像这样重写契约(Contract)，它按预期工作，没有任何警告:

public struct Period
{
    public Period(DateTime start, DateTime end) : this()
    {
        Contract.Requires(start <= end);
        this.start = start;
        this.end = end;
    }

    private readonly DateTime start;
    private readonly DateTime end;

    public static Period operator +(Period p, TimeSpan t)
    {
        Contract.Assume(p.start + t <= p.end + t);   // or use temp variables
        return new Period(p.start + t <= p.end + t);
    }
}

但只需使用 Contract.Assume(p.start <= p.end)不会工作。

CodeContracts: requires unproven: start <= end

Answer 1

我认为问题的一部分可能是您在 Contract.Requires 中使用的条件。打电话。

以您的一个构造函数为例:

public Period(DateTime? start, DateTime? end) : this()
{
    Contract.Requires(!start.HasValue || !end.HasValue || start.Value <= end.Value);
    this.start = start;
    this.end = end;
}

如果 start.HasValue怎么办是 false (意思是 !start.HasValue 是 true )，但是 end确实有值(value)。什么 start.value <= end.Value在这种情况下评估为，因为其中一个是 null而另一个有值(value)吗？

相反，您的 Contract.Requires条件应说明如下:

Contract.Requires(!(start.HasValue && end.HasValue) || start.Value <= end.Value);

如果 start 中的任何一个或 end没有值，则条件返回 true (以及 OR 条件短路，从不评估是否 start.Value <= end.Value )。但是，如果同时 start和 end有一个赋值，条件返回的第一部分 false ，此时， start.Value必须小于或等于 end.Value为了使条件评估为 true总体而言。这就是你所追求的。

这里有一个问题要问您: Period 的任何实例是否属实？要求 start.Value <= end.Value或其中之一(或两者)是 null ?如果是这样，您可以将其指定为 不变量 ，取而代之。这意味着在任何方法进入或退出时， !(start.HasValue && end.HasValue) || start.Value <= end.Value必须成立。当它起作用时，这可以大大简化您的契约(Contract)。

更新

查看我在评论( TDD and Code Contracts )中发布的博客文章，您可以安全地注释您的 operator +(Period p, TimeSpan t)使用代码契约实现 PureAttribute属性。该属性告诉代码契约静态分析器该方法不会改变调用该方法的对象的任何内部状态，因此没有副作用:

[Pure]
public static Period operator +(Period p, TimeSpan t)
{
    Contract.Requires(!(p.start.HasValue && p.end.HasValue) || p.start.Value <= p.end.Value)

    return new Period(
        p.start.HasValue ? p.start.Value + t : (DateTime?) null,
        p.end.HasValue ? p.end.Value + t : (DateTime?) null);
}

更新

好的，我又考虑了这个问题，我想我现在明白代码契约(Contract)与您的契约(Contract)之间存在的问题。我认为您还需要添加 Contract.Ensures与您的构造函数的契约(Contract)(即后置条件契约(Contract)):

public Period(DateTime? start, DateTime? end) : this()
{
    Contract.Requires(!(start.HasValue && end.HasValue) || start.Value <= end.Value);
    Contract.Ensures(!(this.start.HasValue && this.end.HasValue) || this.start.Value <= this.end.Value);
    this.start = start;
    this.end = end;
}

这告诉代码契约，当你的构造函数退出时，对象的 start和 end字段，如果它们都有值，必须满足条件 start.Value <= end.Value .如果不满足该条件，(可能)代码协定将引发异常。这也应该有助于静态分析器。

更新(再次，主要是为了完整性)

我对“未经证实”的警告做了更多的调查。这对于 Requires 都可能发生和 Ensures .这是某人遇到类似问题的另一个示例: http://www.go4answers.com/Example/ensures-unproven-contractresult-79084.aspx .

添加契约不变量可以按如下方式完成(对于 OP 有问题的代码):

[ContractInvariantMethod]
protected void PeriodInvariants()
{
    Contract.Invariant(!(start.HasValue && end.HasValue) || start.Value <= end.Value);
}

此方法将在每次进入/退出对象的方法时调用，以确保此条件成立。

另一个应该证明很有趣的博客条目

我发现其他人的另一篇博客文章可能很有趣: http://www.rareese.com/blog/net-code-contracts

在这种情况下，我不同意作者摆脱 requires unproven 的“解决方案”。警告。这是作者的代码:

public static void TestCodeContract(int value)
{
    if(value > 100 && value < 110)
        TestLimits(value); 
}

public static void TestLimits(int i)
{
    Contract.Requires(i > 100);
    Contract.Requires(i < 110);

    //Do Something
}

在这里，问题的真正解决方案应该如下:

public static void TestCodeContract(int value)
{
    Contract.Requires(value > 100 && value < 110);
    // You could alternatively write two Contract.Requires statements as the blog
    // author originally did.
}

这也应该消除警告，因为静态分析器现在知道 value必须在 101 到 109 的范围内，这也恰好满足 TestLimits 的合约标准方法。

因此，我对您的建议是检查 Period 的任何位置。构造函数被调用，和/或 Period.operator +(...)方法来确保调用方法也有必要的 Contract.Requires语句(或者， Contract.Assume ，它告诉静态分析器只假设提供的条件为真)。

使用代码契约时，您需要检测所有代码。您通常无法“挑选”指定契约(Contract)的部分，因为静态分析器很可能没有足够的信息来完成其分析(因此，确保契约(Contract)得到保证)并且您将收到许多警告.