为什么 CodeContracts 静态检查器在我 Contract.Ensure(a) 之后建议我 Contract.Assume(a)？答案

【问题标题】：why is CodeContracts static checker suggesting that I Contract.Assume(a) right after I Contract.Ensure(a)?为什么 CodeContracts 静态检查器在我 Contract.Ensure(a) 之后建议我 Contract.Assume(a)？
【发布时间】：2013-06-30 07:39:51
【问题描述】：

基本上，我有一个虚拟方法可以将某些强制性后置条件传播到子类。这是一个简化版本和静态检查器生成的奇怪警告（编辑 - 我的示例不完整。现在）：

public abstract class InitializerClass
{
    protected bool _initialized

    public bool IsInitialized
    {
        get { return _initialized; }
    }

    public virtual void Initialize()
    {
        //Warning CodeContracts: Missing precondition in an externally visible
        //method. Consider adding Contract.Requires(this.IsInitialized); for
        //parameter validation
        Contract.Ensures(IsInitialized);
    }
}

这是另一个类：

public abstract class OrderingClass
{
    protected bool _ordered

    public bool IsOrdered
    {
        get { return _ordered; }
    }

    public override void Initialize()
    {
        //Message CodeContracts: Suggested assume: Contract.Assume(this.IsOrdered);
        Contract.Ensures(IsOrdered);
    }
}

事实上，两个警告都指向方法的右花括号，在 Contract.Ensure 调用下面的行中。我的代码有什么问题？

【问题讨论】：

我显然不能将Contract.Requires(IsInitialized) 添加到InitializerClass.Initialize，因为确保IsInitialized 设置为true 作为后置条件是合同的重点。这些东西是相互排斥的。与 OrderingClass.Initialize 覆盖相同。我错过了什么还是静态检查器真的很困惑？
方法里其实有代码设置_initialized为true吧？最好加上清楚。
使用 CodeContracts 版本 1.7.11202.10 静态检查不会产生这样的警告，警告级别和选项都会提高，无论我尝试如何修复代码（除了 Henk 的评论：缺少半列，覆盖没有基类）。

标签： c# inheritance abstract-class code-contracts post-conditions

【解决方案1】：

您收到此错误是因为代码协定无法验证调用 Initialize() 是否会导致 IsInitialized 返回 true。这是因为Initialize() 的主体中没有将IsInitialized 的值设置为true 的代码，因此分析器会警告您代码假设IsInitialized 在进入true 时为true @，并且你应该明确这个前提条件。

有两种方法可以消除警告。

首先，添加建议的前置条件：

public virtual void Initialize()
{
    Contract.Requires(IsInitialized);
    Contract.Ensures(IsInitialized);
}

其次，将IsInitialized的值设置为true：

public virtual void Initialize()
{
    IsInitialized = true;
    Contract.Ensures(IsInitialized);
}

您需要向IsInitialized 添加一个私有setter 才能使上述代码正常工作。

public bool IsInitialized
{
    get { return _initialized; }
    private set { __initialized = value; }
}

在Initialize() 中简单地设置_initialized = true 可能不允许代码契约验证后置条件，因此添加了私有设置器。但是，话虽如此，将以下合约添加到 IsInitialized 可能会否定添加属性设置器的需要：

public bool IsInitialized
{
    get
    {
        Contract.Ensures(Contract.Result<bool>() ^ !_initialized);
        return _initialized; 
    }
}

出于完全相同的原因，您在OrderingClass 收到警告。 Code Contracts 建议使用Contract.Assume()，因为您不能在覆盖中使用Contract.Requires()。

【讨论】：