静态检查器无法在某些条件下评估确定性行为？答案

【问题标题】：Static checker can't assess deterministic behaviour under certain conditions?静态检查器无法在某些条件下评估确定性行为？
【发布时间】：2012-08-15 12:14:47
【问题描述】：

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

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

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

//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;
}

【问题讨论】：

在挑剔之前：这是测试代码。不要担心格式、变量名、标准等，除非它们与静态分析相关！
这不是一个答案，但静态 CC 检查器非常弱。它不能证明对实际程序有用的属性。

标签： c# code-contracts static-code-analysis deterministic

【解决方案1】：

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

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

【讨论】：