1

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

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 调用下面的行中。我的代码有什么问题？

4

1 回答 1

0

您收到此错误是因为代码合同无法验证调用Initialize()是否会IsInitialized返回 true。这是因为在设置toInitialize()的值的主体中没有代码，因此分析器警告您该代码假设正在进入 to ，并且您应该明确此前提条件。IsInitializedtrueIsInitializedtrueInitialize()

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

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

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

其次，将值设置IsInitialized为true：

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

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

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

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

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

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

于 2016-04-12T10:29:02.593 回答