Cannot use ContractAbbreviator in ContractClass?

Question

I've just started using code-contracts and found that the ContractAbbreviator attribute makes it possible to describe contracts in a clean way.

However, I'm not able to make it work in a contract class for an abstract class.

Given this simple class:

[ContractClass(typeof(MyContractClass))]
internal abstract class MyClass
{
    public abstract int Position { get; }

    public abstract void Reset();
}

I'd like to write a contract class that ensures that:

• Position is always greater than or equal to zero.
• Position is zero for newly created instances.
• Reset() causes Position to revert to it's initial value (zero).

So, I came up with this contract class:

[ContractClassFor(typeof(MyClass))]
internal abstract class MyContractClass : MyClass
{
    internal MyContractClass()
    {
        this.EnsuresInitialState();
    }

    public override int Position
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() >= 0);
            return default(int);
        }
    }

    public override void Reset()
    {
        this.EnsuresInitialState();
    }

    [ContractAbbreviator]
    private void EnsuresInitialState()
    {
        Contract.Ensures(this.Position == 0);
    }
} 

However, when compiling this I get the following error:

Contract class MyContractClass references member MyContractClass.EnsuresInitialState which is not part of the abstract class/interface being annotated.

Does that mean that it's impossible to use ContractAbbreviator methods in a contract class, or am I doing something wrong here?

In this simple class there is really no point in having an abbreviator, since the state to ensure is just a single property. In my real class, however, there are several other properties that I want to ensure are reverted back to their initial values.

I'm using Visual Studio 2013 Update 4.

Answer 1

Move the EnsuresInitialState method to the abstract class and mark it protected. Then add a default constructor to the abstract class that calls it:

[ContractClass(typeof(MyContractClass))]
internal abstract class MyClass
{
    protected MyClass()
    {
        EnsuresInitialState();
    }

    [ContractAbbreviator]
    protected void EnsuresInitialState()
    {
        Contract.Ensures(Position == 0);
    }

    public abstract int Position { get; }

    public abstract void Reset();
}

[ContractClassFor(typeof(MyClass))]
internal abstract class MyContractClass : MyClass
{
    public override int Position
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() >= 0);
            return default(int);
        }
    }

    public override void Reset()
    {
        EnsuresInitialState();
    }
}