c# - 不能在 ContractClass 中使用 ContractAbbreviator？

Question

我刚开始使用 code-contracts并发现 ContractAbbreviator属性使得以简洁的方式描述契约(Contract)成为可能。

但是，我无法让它在抽象类的契约类中工作。

给定这个简单的类:

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

    public abstract void Reset();
}

我想编写一个契约类来确保:

• Position 始终大于或等于零。
• Position 对于新创建的实例为零。
• Reset() 导致 Position 恢复到它的初始值(零)。

所以，我想到了这个契约类:

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

但是，编译时出现以下错误:

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

这是否意味着不可能使用 ContractAbbreviator契约(Contract)类中的方法，还是我在这里做错了什么？

在这个简单的类中，使用缩写词真的毫无意义，因为要确保的状态只是一个属性。然而，在我的真实类(class)中，还有其他几个属性我想确保恢复到它们的初始值。

我正在使用 Visual Studio 2013 Update 4。

Answer 1

将 EnsuresInitialState 方法移至抽象类并将其标记为 protected 。然后在调用它的抽象类中添加一个默认构造函数:

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