如何將實現添加到接口代碼合同時繼承關閉接口

Question

我的例子是一種情況，繼承基接口的接口需要添加其附加字段的結果的後置條件 - 這個例子發生在我決定有一個IInitialise接口作爲從此繼承的接口，總是希望將一個前置/後置條件添加到Initialise方法中。

我可以看到問題是由於抽象實現無法避免彼此（或者由於攔截或重寫）。

[ContractClass(typeof(IInitialiseContract))] 
    public interface IInitialise 
    { 
     bool IsInitialised { get; } 
     void Initialise(); 

    } 

    [ContractClassFor(typeof(IInitialise))] 
    public abstract class IInitialiseContract : IInitialise 
    { 

     public bool IsInitialised 
     { 
      get { return default(bool); } 
     } 

     public void Initialise() 
     { 
      Contract.Ensures(IsInitialised == true); 
     } 
    } 

後來我結束了以下接口

[ContractClass(typeof(IEnginecontract))] 
    public interface IEngine : IInitialise 
    { 
     ICommandManager CommandManager { get; } 
     IDictionary<int, IEntity> World { get; } 
    } 

    [ContractClassFor(typeof(IEngine))] 
    public abstract class IEnginecontract : IEngine 
    { 

     public ICommandManager CommandManager 
     { 
      get 
      { 
       Contract.Ensures(Contract.Result<ICommandManager>() != null); 
       return default(ICommandManager); 
      } 
     } 

     public IDictionary<int, IEntity> World 
     { 
      get 
      { 
       Contract.Ensures(Contract.Result<IDictionary<int, IEntity>>() != null); 
       return default(IDictionary<int, IEntity>); 
      } 
     } 

     public bool IsInitialised 
     { 
      get { return default(bool); } 
     } 

     public void Initialise() 
     { 
      // I would like to put my pre and post conditions here but 
      // cannot because it is implemented in the base interfaces contract. 
     } 
    } 

我到這裏，我想不出一個乾淨的方式來增加條件初始化（）。

EDIT2：如果我把這個方法需要的，我會得到一個錯誤這樣

警告1合同類作爲其原始定義的類型不IEngine IEngine不能定義方法IInitialise.Initialise合同。改爲在IInitialise類型上定義合同。 IEngine .cs

任何想法？

Answer 1

我不認爲這是可能的。我廣泛地使用代碼契約，據我所知 - 我記得自己嘗試過類似的東西 - 您的派生接口的代碼契約必須再次包含所有條件，它不能繼承它們。

Answer 2

任何來自您正在編寫合同的界面以外的任何方法都應標記爲abstract。這些方法的契約將自動繼承，並且不能更改它們（否則這會改變基本接口的含義，這是沒有意義的）。

所以，你應該有你的基本接口和契約：

[ContractClass(typeof(IInitialiseContract))] 
public interface IInitialise 
{ 
    bool IsInitialised { get; } 
    void Initialise(); 

} 

[ContractClassFor(typeof(IInitialise))] 
public abstract class IInitialiseContract : IInitialise 
{ 

    public bool IsInitialised 
    { 
     get { return default(bool); } 
    } 

    public void Initialise() 
    { 
     Contract.Ensures(IsInitialised == true); 
    } 
} 

而派生的接口和它的合同（注意抽象的繼承者）：

[ContractClass(typeof(IEnginecontract))] 
public interface IEngine : IInitialise 
{ 
    ICommandManager CommandManager { get; } 
    IDictionary<int, IEntity> World { get; } 
} 

[ContractClassFor(typeof(IEngine))] 
public abstract class IEnginecontract : IEngine 
{ 

    public ICommandManager CommandManager 
    { 
     get 
     { 
      Contract.Ensures(Contract.Result<ICommandManager>() != null); 
      return default(ICommandManager); 
     } 
    } 

    public IDictionary<int, IEntity> World 
    { 
     get 
     { 
      Contract.Ensures(Contract.Result<IDictionary<int, IEntity>>() != null); 
      return default(IDictionary<int, IEntity>); 
     } 
    } 

    public abstract bool IsInitialised {get;} 
    public abstract void Initialise(); 
}