代码契约：抽象类中的不变量答案

【问题标题】：Code Contracts: Invariants in abstract class代码契约：抽象类中的不变量
【发布时间】：2015-03-20 20:47:41
【问题描述】：

我在使用带有代码协定的不变量时遇到了一个问题。我想在我的抽象类中定义一个不变量，但它只是被忽略了。下面的代码显示了我的接口和抽象类。

[ContractClass(typeof(IPointContract))]
interface IPoint
{
    int X { get; }
    int Y { get; }
}

[ContractClassFor(typeof(IPoint))]
abstract class IPointContract : IPoint
{

    public int X
    {
        get { return 0; }

    }

    public int Y
    {
        get { return 0; }
    }

    [ContractInvariantMethod]
    private void PointInvariant()
    {
        Contract.Invariant(X > Y);
    }
}

之后，我在我的 Point 类中实现了这个接口，并从中创建了一个对象。这至少应该在运行时失败。

class Point : IPoint
{
    public Point(int X, int Y)
    {
        this._x = X;
        this._y = Y;
    }

    private int _x;
    public int X
    {
        get { return _x; }
    }

    private int _y;
    public int Y
    {
        get { return _y; }
    }
}

class Program
{
    static void Main(string[] args)
    {
        Point p = new Point(1, 2);
    }
}

当我将不变量移到点类时，它工作正常。所有其他前置或后置条件也都可以正常工作。

在抽象类中不可能有不变量还是我做错了？

【问题讨论】：

为什么要用接口语义来命名抽象类？抽象类不是接口，不应以 I 开头。
我使用的语义与代码合同手册中的语义相同。见第 2.8 章research.microsoft.com/en-us/projects/contracts/userdoc.pdf
我明白了……这不是 I-FooContract，而是 IFoo-Contract。如果是我，我可能会把它写成 ContractForIFoo 以便清楚，但也许这里有一些约定......
第一个问题很好！

标签： c# abstract-class code-contracts invariants

【解决方案1】：

接口不支持不变量。（您的问题标题是“抽象类中的不变量”，但问题的症结在于接口。）

我的猜测是，这是因为不变量需要状态，但接口没有状态。我确信代码合同团队可以解决这个问题，我希望他们会这样做，因为这将是一个很棒的功能。

要解决此限制，您可以：

将不变方法添加到派生类（class Point 等）。
或者，将 setter 添加到抽象类属性并在 setter 中实现协定逻辑。

【讨论】：