我是很新，设计由合同的概念，但到目前为止，我爱它使多么容易找到潜在的错误。
不过，我一直在与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功能。
我曾尝试与finagling Invariant S，但并没有看到证明，以帮助Ensures约束。
任何帮助就如何通过接口证明将是有益的。
EDIT1：
当我将其添加到MyAwesomePlugin类：
[ContractInvariantMethod]
protected void ObjectInvariant()
{
Contract.Invariant(((IPlugin)this).State == this.state);
}
试图暗示状态作为IPlugin是一样的我的私有状态，我得到同样的警告，并认为“私人诠释？数=零”线不能证明不变的警告。
考虑到这是在静态构造函数的第一个可执行行，我可以看到它为什么可以这样说，但为什么不能够证明的Ensures ？
EDIT2
当我标志着State与[ContractPublicPropertyName("State")]我得到一个错误，指出“没有公共领域/评为‘国家’有型‘MyNamespace.State’属性，可以发现”
看起来这应该把我拉近，但我不能令人信服。
