c# - 价值类型的代码契约

Question

我刚刚开始使用代码合约，虽然很有希望，但它们似乎在值类型方面有一些限制。例如：

public struct Wrap<T>
    where T : class
{
    readonly T value;
    public Wrap(T value)
    {
        Contract.Requires(value != null);
        this.value = value;
    }
    public T Value
    {
        get
        {
            Contract.Requires(Value != null);
            return value;
        }
    }
    [Pure]
    [ContractInvariantMethod]
    void Invariant()
    {
        Contract.Invariant(value != null);
    }
    public static T BigError()
    {
        Contract.Ensures(Contract.Result<T>() != null);
        var x = default(Wrap<T>);
        Contract.Assert(x.Value != null);
        return x.Value;
    }
}

Wrap.BigError 清楚地说明了这个问题。此示例编译并 ccheck 验证 4 个断言，但断言在运行时显然会失败。其中一些断言是多余的，我插入它们只是为了确保验证者在指定点检查这些属性。

我没有看到这种事情在MS 的代码合同文档中被列为已知问题，但它似乎太明显了，不能作为遗漏。我错过了什么吗？

Answer 1

原来问题是结构中指定的不变量。如果删除不变量，则会得到预期的错误。与 MS 的文档相反，静态检查器似乎确实考虑了结构不变量。

Answer 2

您的 Value 属性的吸气剂合同中有一些奇怪的东西。您递归地要求 this.Value != null。我确定你的意思是别的，例如

Contract.Ensures( Contract.Result<T>() != null );

有了这个修复，规范对我来说看起来非常合理。检查器（包括运行时）的限制是您始终可以创建结构的默认值，我们无法检查这些默认值的不变量。因此，检查是以默认值的构造为模的。