Design by Contract: Can you have an Interface with a Protocol?

Question

Hi all, I'm pretty new to the concept of Design by Contract, but so far, I'm loving how easy it makes it to find potential bugs.

However, I've been working with the Microsoft.Contracts library (which is pretty great,) and I have run into a road block.

Take this simplified example of what I'm trying to do:

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

To sum it up, I am declaring an interface for plugins to follow, and requiring them to declare their state, and limiting what can be called in any state.

This works at the call site, for both static and runtime validation. But the warning I keep getting is "contracts: ensures unproven" for both the Reset and Prepare functions.

I have tried finagling with Invariants, but that doesn't seen to aid in proving the Ensures constraint.

Any help as to how to prove through the interface would be helpful.

EDIT1:

When I add this to the MyAwesomePlugin class:

    [ContractInvariantMethod]
    protected void ObjectInvariant()
    {
        Contract.Invariant(((IPlugin)this).State == this.state);
    }

Attempting to imply that the state as an IPlugin is the same as my private state, I get the same warnings, AND a warning that the "private int? number = null" line fails to prove the invariant.

Given that that is the first executable line in the static constructor I can see why it may say so, but why doesn't that prove the Ensures?

EDIT2

When I mark State with [ContractPublicPropertyName("State")] I get an error saying that "no public field/property named 'State' with type 'MyNamespace.State' can be found"

Seems like this should put me closer, but I'm not quite there.

Answer 1

With this code snippet, I effectively suppressed the warning:

    void IPlugin.Reset()
    {
        this.number = null;
        this.state = State.NotReady;
        Contract.Assume(((IPlugin)this).State == this.state);
    }

This actually answers my first question, but asks a new one: Why didn't the invariant help prove this?

I will be posting a new question.