为什么CodeContracts静态检查器暗示我合同。假设（a）在合同签订之后。确保（a）？

基本上，我有一个虚拟方法来传播某些强制后置条件到子类。下面是一个简化版本和奇怪的警告静态检查生成（编辑 - 我的例子是不完整这是现在。）：为什么CodeContracts静态检查器暗示我合同。假设（a）在合同签订之后。确保（a）？

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

来源

2013-06-30 user2212990

我显然无法将'Contract.Requires（IsInitialized）'添加到'InitializerClass.Initialize'中，因为确保'IsInitialized'设置为true，因为后期条件是合同的要点。这些东西是相互排斥的。 'OrderingClass.Initialize'覆盖也是一样。我是否错过了一些东西，或者是静态检查器只是很困惑？ – user2212990

实际上在代码中设置了_initialized为true的方法，对吧？最好加上它来清楚。 –

使用CodeContracts版本1.7.11202.10静态检查时，不管使用何种方法修复代码（除了Henk的评论：缺少半列，没有基类的重写），警告级别和选项都会启动。 – Stein

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

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

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

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

简单地设置在Initialize()_initialized = true可能不会允许代码契约验证后置条件，因此增加私人二传手。不过，话说回来，添加以下合同IsInitialized否定了需要添加属性setter：

你所得到的预警OrderingClass的确切同样的原因。代码合同建议Contract.Assume()，因为您不能在覆盖中使用Contract.Requires()。

来源

2016-04-12 10:29:02

为什么CodeContracts静态检查器暗示我合同。假设（a）在合同签订之后。确保（a）？

回答

相关问题