Reputation: 4836
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?
Upvotes: 4
Views: 1927
Reputation: 30580
Any methods which are from an interface other than the one you're writing the contracts for should be marked abstract
. The contracts for these methods will be inherited automatically, and you can't change them (or this would alter the meaning of the base interface, which doesn't make sense).
So you should have your base interface and its contracts:
[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);
}
}
And your derived interface and its contracts (note abstract inherited ones):
[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();
}
Upvotes: 3
Reputation: 33139
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.
Upvotes: 2