3

我已设法将其归结为以下测试用例，但我想知道这是否是 C# 代码合同中静态检查器的限制，还是我缺少的东西。当我尝试使用一种代码来证明合同时，它会抛出一个不变的未经证实的警告，但是（我认为是）一种证明它可以正常工作的等效方法。

最初我认为这可能是因为我没有使用具有 Pure 属性的对象（因此代码合同无法评估属性是否是确定性的）而是在对象周围创建了 Pure 包装器（恰好是Nullable<Int64>）没有帮助。

第一个和第三个测试用例之间是否有区别，或者我认为它们是等价的是否正确，只是静态检查器无法正确评估第三种情况？

//Works

private Int64? _violations = null;

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(CheckIsValid(_violations));
}

[Pure]
public static Boolean CheckIsValid(Int64? value)
{
    return (value.HasValue ? value.Value >= 0 : true);
}

public Class1(Int64 violations)
{
    Contract.Requires(violations >= 0);
    Contract.Ensures(CheckIsValid(_violations));
    _violations = violations;
}


//Doesn't work, not provably deterministic

private Int64? _violations = null;

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(_violations.HasValue ? _violations.Value >= 0 : true);
}

public Class1(Int64 violations)
{
    Contract.Requires(violations >= 0);
    Contract.Ensures(_violations.HasValue ? _violations.Value >= 0 : true);
    _violations = violations;
}

//Also doesn't work, even though it's provably deterministic

private PureNullableInt64 _violations = null; //A wrapper class around Int64? with [Pure] getters

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(_violations.HasValue ? _violations.Value >= 0 : true);
}

public Class1(Int64 violations)
{
    Contract.Requires(violations >= 0);
    Contract.Ensures(_violations.HasValue ? _violations.Value >= 0 : true);
    _violations = violations;
}
4

1 回答 1

2

所有三个版本都相同，您的第一个版本也不起作用。看起来确实如此，因为您将警告级别设置得足够低，以至于警告被掩盖了。尝试将警告级别设置为最高，您将看到“确保未经证实”警告。

问题是没有合同说new Nullable<T>(x).Value == x。只有合同上写着new Nullable<T>(x).HasValue。这不足以证明你的不变量。应该为基类指定许多合同，但还没有。您可以将其带到代码合同论坛并请求添加。

于 2012-09-03T13:13:18.753 回答