Code Contracts: How to deal with inherited interfaces?

Question

I'm using MS Code Contracts and have run into a snag with using interface inheritance and ContractClassFor attributes.

Given these interfaces and contract classes:

[ContractClass(typeof(IOneContract))]
interface IOne { }
[ContractClass(typeof(ITwoContract))]
interface ITwo : IOne { }

[ContractClassFor(typeof(IOne))]
abstract class IOneContract : IOne { }
[ContractClassFor(typeof(ITwo))]
abstract class ITwoContract : IOneContract, ITwo { }

Let's say that IOne and ITwo are substantial interfaces. So IOneContract would have a significant amount of code in it for the necessary checks.

I don't want to duplicate all of that in ITwoContract for the IOne interfaces. I only want to add new contracts for the ITwo interfaces. Inheriting one contract class from another seems the likely way to reuse that code. Yet I get the following error:

EXEC : warning CC1066: Class 'ITwoContract' is annotated as being the contract for the interface 'ITwo' and cannot have an explicit base class other than System.Object.

Is this a limitation in Code Contracts or am I doing it wrong? We have a lot of interface inheritance in our project and this feels like a deal breaker for Code Contracts if I can't figure out how to work around this issue.

Answer 1

Instead of:

[ContractClassFor(typeof(ITwo))]
abstract class ITwoContract : IOneContract, ITwo { }

Just inherit the contract:

[ContractClassFor(typeof(ITwo))]
abstract class ITwoContract : ITwo { }

You only need to provide contracts on the methods which are new in ITwo. The contracts from IOneContract will be inherited automatically, and you can declare all the inherited IOne methods as abstract — in fact, you cannot provide contracts for IOne on ITwoContract, or CC will complain :)

For example, if you have this:

[ContractClass(typeof (IOneContract))]
interface IOne
{
    int Thing { get; }
}

[ContractClass(typeof (ITwoContract))]
interface ITwo : IOne
{
    int Thing2 { get; }
}

[ContractClassFor(typeof (IOne))]
abstract class IOneContract : IOne
{
    public int Thing
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() > 0);
            return 0;
        }
    }
}

[ContractClassFor(typeof (ITwo))]
abstract class ITwoContract : ITwo
{
    public int Thing2
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() > 0);
            return 0;
        }
    }

    public abstract int Thing { get; }
}

Then this implementation will say "unproven contract" on both methods, as expected:

class Two : ITwo
{
    public int Thing
    {
        get { return 0; }
    }

    public int Thing2
    {
        get { return 0; }
    }
}