为什么CodeContracts静态检查器建议I Contract.Asseume(a)紧跟在I Contract.Ae

Question

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

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.Esure调用后面的行中。我的代码出了什么问题？

Answer 1

您收到此错误是因为代码约定无法验证调用Initialize()是否会导致IsInitialized返回true。这是因为Initialize()的主体中没有将IsInitialized的值设置为true的代码，因此分析器警告您，该代码假设IsInitialized在进入Initialize()时为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可能不允许代码契约验证post条件，因此添加了私有setter。然而，已经说过，在IsInitialized中添加以下合同可能会否定添加属性设置器的必要性：

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

您在OrderingClass中收到警告的原因完全相同。代码协定建议使用Contract.Assume()，因为您不能在重写中使用Contract.Requires()。