我可以获得代码合同来警告我有关“非法”的行为吗？子类型？

Question

抱歉，如果这个问题看起来太长。在我提出问题之前，我需要先表明它来自哪里。

设置：

给定以下不可变类型 Rectangle：

class Rectangle
{
    public Rectangle(double width, double height) { … }

    public double Width  { get { … } }
    public double Height { get { … } }
}

... 从它派生类型 Square 似乎完全合法：

using System.Diagnostics.Contracts;

class Square : Rectangle
{
    public Square(double sideLength) : base(sideLength, sideLength) { }

    [ContractInvariantMethod]
    void WidthAndHeightAreAlwaysEqual()
    {
        Contract.Invariant(Width == Height);
    }
}

... 因为派生类可以确保其自身的不变性从未被侵犯。

但是，一旦我使 Rectangle 可变：

class Rectangle
{
    public double Width  { get; set; }
    public double Height { get; set; }
    …
}

...我就不应该再从中派生 Square，因为 Square 不应该有独立的设置器宽度和高度。

问题：

我可以如何处理代码契约，以便在我从可变 Rectangle 类派生 Square 时立即警告我违反契约？最好是，Code Contracts 的静态分析已经在编译时向我发出警告。

换句话说，我的目标是使用代码契约对以下规则进行编码：

• 矩形的Width和Height可以彼此独立地更改。
• Square 的 Width 和 Height 不能彼此独立地更改，这从一开始就没有意义。

……并以这样的方式进行：每当这些规则发生“冲突”时，代码合约就会注意到。

到目前为止我所考虑的：

1。向矩形添加不变量：

class Rectangle
{
    …
    [ContractInvariantMethod]
    void WidthAndHeightAreIndependentFromOneAnother()
    {
        Contract.Invariant(Width != Height || Width == Height);
    }
}

这种方法的问题是，虽然不变量正确地指出“宽度和高度不必相等，但它们可以相等”，但它是无效，(1) 因为它是同义反复，(2) 因为它比派生类 Square 中的不变 Width == Height 限制更少。也许它甚至在代码契约看到它之前就被编译器优化掉了。

2.向 Rectangle 的设置器添加后置条件：

public double Width
{
    get { … }
    set { Contract.Ensures(Height == Contract.OldValue(Height)); … }
}

public double Height
{
    get { … }
    set { Contract.Ensures(Width == Contract.OldValue(Width)); … }
}

这将禁止派生类 Square 简单地将 Height 更新为 每当 Width 更改时，它不会阻止我从 Square 类派生 Square 类，反之亦然。 >矩形。但这就是我的目标：让代码契约警告我 Square 不得从可变的 Rectangle 派生。

Answer 1

最近的 MSDN 杂志中有一篇非常相关的文章，讨论了基本相同的问题： “代码契约：继承和里氏原则” - 我无法想出更好的答案。

您所认为的“非法”子类型基本上违反了里氏替换原则，本文展示了代码合约如何帮助检测此问题。

Answer 2

MSDN 杂志 2011 年 7 月号中有一篇文章描述了很多你的问题，用同样的例子，并讨论代码契约的使用和里氏替换原则。

Answer 3

感谢 @BrokenGlass 和 @Mathias 提供了最近 MSDN 杂志文章的链接，该文章名为 代码契约：继承和里氏原则。虽然我认为其中有问题（我稍后会解决这个问题......请参阅此答案的第二部分），但它帮助我决定了解决方案。

我决定的解决方案：

1. 我将以下后置条件添加到基类Rectangle：

   公共双宽度
   {
       设置 { Contract.Ensures(Height == Contract.OldValue(Height)); }
   }
   
   公共双高
   {
       设置 { Contract.Ensures(Width == Contract.OldValue(Width)); }
   }
   

   这些基本上断言宽度和高度可以彼此独立设置。

2. 在派生类Square中添加一个不变量：

   Contract.Invariant(宽度==高度);
   

   这基本上表明了相反的情况。

总而言之，这些将最终导致合同违规——诚然不是在编译时，但似乎只能在某些极端情况下使用代码合同来完成（即，当派生类开始添加前提条件。）

为什么 MSDN 杂志文章中的解决方案没有帮助？

MSDN 文章似乎展示了一种具有编译时警告优势的解决方案。为什么我坚持使用上面没有这个好处的解决方案？

简答：

代码示例中的一个无法解释的变化清楚地表明，本文设置了一个人为的情况，以展示代码契约的静态分析。

长答案：

本文以 Rectangle 类的代码示例（→ 图 1）开始，其中包含 Width 和 的单独设置器>高度。下次显示 Rectangle 类时（→图 2），setter 已设为私有，并且只能通过添加的方法 SetSize(width,高度）。

文章没有说解释为什么默默地引入这个改变。事实上，这种更改在单独的 Rectangle 上下文中可能根本没有任何意义，除非您当然已经知道您将派生一个类似 Square 的类，您可以在其中派生一个类似 Square 的类。需要添加一个前置条件宽度==高度。当 Width 和 Height 的设置器彼此分离时，您无法将其添加为先决条件。如果您无法添加该前提条件，您将不会从代码契约中收到编译时警告。