Search code examples
c#interfacecode-contracts

How to Add implementation to Interface code contract when inheriting off interface


My example is a situation where the interfaces that inherit of the base interface need to add post conditions that are a result of their additional fields - the example occured when i decided to have an IInitialise interface as interfaces that inherit from this invariably want a pre/post condition added to the Initialise method.

I can see that the problem is due to the abstract implementations having no way to avoid each other (either due to interception or the rewriter).

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

then later I end up with the following interface

  [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.
        }
    }

I get to here and i cannot figure out a nice clean way to add conditions to Initialise().

Edit2: If I had put a requires in this method i would of got an error like this

Warning 1 Contract class IEngine cannot define contract for method IInitialise.Initialise as its original definition is not in type IEngine . Define the contract on type IInitialise instead. IEngine .cs

Any ideas?


Solution

  • I don't think it's possible. I use code contracts extensively and as far as I can tell -- I remember having tried something like this myself -- your derived interface's code contract must include all conditions again, it cannot inherit them.