我对 Contract 式设计的概念很陌生，但到目前为止，我很喜欢找到潜在的错误是多么容易 .
但是，我一直在使用Microsoft.Contracts库（非常棒），我遇到了障碍 .
以我正在尝试做的简化示例为例：
public enum State { NotReady, Ready }
[ContractClass(typeof(IPluginContract))]
public interface IPlugin
{
State State { get; }
void Reset();
void Prepare();
void Run();
}
[ContractClassFor(typeof(IPlugin))]
public class IPluginContract : IPlugin
{
State IPlugin.State { get { throw new NotImplementedException(); } }
void IPlugin.Reset()
{
Contract.Ensures(((IPlugin)this).State == State.NotReady);
}
void IPlugin.Prepare()
{
Contract.Ensures(((IPlugin)this).State == State.Ready);
}
void IPlugin.Run()
{
Contract.Requires(((IPlugin)this).State == State.Ready);
}
}
class MyAwesomePlugin : IPlugin
{
private State state = State.NotReady;
private int? number = null;
State IPlugin.State
{
get { return this.state; }
}
void IPlugin.Reset()
{
this.number = null;
this.state = State.NotReady;
}
void IPlugin.Prepare()
{
this.number = 10;
this.state = State.Ready;
}
void IPlugin.Run()
{
Console.WriteLine("Number * 2 = " + (this.number * 2));
}
}
总而言之，我正在声明一个接口插件，并要求它们声明它们的状态，并限制在任何状态下可以调用的内容 .
这适用于调用站点，用于静态和运行时验证 . 但对于 Reset 和 Prepare 函数，我一直得到的警告是"contracts: ensures unproven" .
我尝试过使用 Invariant s，但这并没有帮助证明 Ensures 约束 .
有关如何通过界面进行验证的任何帮助都会有所帮助 .
EDIT1:
当我将它添加到MyAwesomePlugin类时：
[ContractInvariantMethod]
protected void ObjectInvariant()
{
Contract.Invariant(((IPlugin)this).State == this.state);
}
试图暗示作为IPlugin的状态与我的私有状态相同，我得到相同的警告，并且警告“private int？number = null”行无法证明不变量 .
鉴于这是静态构造函数中的第一个可执行行，我可以看出它为什么这么说，但为什么不能证明 Ensures ？
EDIT2
当我用 [ContractPublicPropertyName("State")] 标记 State 时出现错误，说"no public field/property named 'State' with type 'MyNamespace.State' can be found"
这样看起来应该让我更接近，但我不是那里 .
1 回答
使用此代码段，我有效地抑制了警告：
这实际上回答了我的第一个问题，但问了一个新的问题：为什么不变的帮助证明了这一点？
我将发布一个新问题 .