Conception par contrat: Pouvez-vous avoir une interface avec un protocole?

Question

Je suis assez nouveau dans le concept de Design by Contract, mais jusqu'à présent, j'adore le fait qu'il soit facile de trouver des bogues potentiels.

Cependant, j'ai travaillé avec la bibliothèque Microsoft.Contracts (ce qui est plutôt génial) et j'ai rencontré un blocage.

Prenez cet exemple simplifié de ce que je suis en train de faire:

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

Pour résumer, je déclare une interface pour les plugins à suivre, et les obligeant à déclarer leur état, et de limiter ce peut être appelé dans n'importe quel état.

Ceci fonctionne sur le site d'appel, pour la validation statique et l'exécution. Mais l'avertissement que je reçois toujours est "contrats: assure non prouvée" pour les fonctions Reset et Prepare.

J'ai essayé de finagling avec Invariant s, mais cela ne semble pas aider à prouver la contrainte Ensures.

Toute aide sur la façon de prouver à travers l'interface serait utile.

EDIT1:

Quand je l'ajouter à la classe MyAwesomePlugin:

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

Toute tentative de laisser entendre que l'État en tant IPlugin est le même que mon état privé, je reçois les mêmes avertissements , ET un avertissement que la ligne "private int? Number = null" ne parvient pas à prouver l'invariant. Etant donné que c'est la première ligne exécutable dans le constructeur statique, je peux voir pourquoi il peut le dire, mais pourquoi cela ne prouve-t-il pas le Ensures?

EDIT2

Quand je marque State avec [ContractPublicPropertyName("State")] je reçois une erreur disant que « aucun champ public/propriété nommée « Etat » avec le type « MyNamespace.State » peut être trouvé »

On dirait Cela devrait me rapprocher, mais je ne suis pas tout à fait là.

Answer 1

Avec cet extrait de code, je l'avertissement effectivement supprimé:

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

Cela répond en fait ma première question, mais demande un nouveau: Pourquoi ne pas l'aide invariante prouver?

Je vais poster une nouvelle question.