Can I get Code Contracts to warn me about "illegal" subtyping?

Question

Sorry if this question seems too long. Before I can ask it, I need to show where it's coming from.

Set-up:

Given the following immutable type Rectangle:

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

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

… it seems perfectly legal to derive a type Square from it:

using System.Diagnostics.Contracts;

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

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

… because the derived class can make sure that its own invariant isn't ever violated.

But as soon as I make Rectangle mutable:

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

… I should no longer derive Square from it, because Square shouldn't ever have independent setters for Width and Height.

Question:

What can I do with Code Contracts such that it will warn me of a contract violation as soon as I derive Square from the mutable Rectangle class? Preferably, Code Contracts' static analysis would already give me a warning at compile-time.

In other words, my goal is to encode the following rules with Code Contracts:

• Width and Height of a Rectangle may be changed independently from one another.
• Width and Height of a Square cannot be changed independently from one another, and that wouldn't be meaningful in the first place.

… and do it in such a way that Code Contracts will notice whenever these rules "collide".

What I've considered so far:

1. Adding an invariant to Rectangle:

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

The problem with this approach is that while the invariant correctly states, "Width and Height don't have to be equal, but they can be", it is ineffectual, (1) because it is a tautology, and (2) because it is less restrictive than the invariant Width == Height in the derived class Square. Perhaps it's even optimised away by the compiler before Code Contracts ever sees it.

2. Adding post-conditions to Rectangle's setters:

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

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

This will forbid the derived class Square from simply updating Height to Width whenever Width is changed and vice versa, it won't stop me per se from deriving a Square class from Rectangle. But that's my goal: getting Code Contracts to warn me that Square must not be derived from a mutable Rectangle.

Answer 1

Thanks to @BrokenGlass and @Mathias for the link to the recent MSDN Magazine article named Code Contracts: Inheritance and the Liskov Principle. While I believe there's something wrong in it (I'll get to that in a second… see the second part of this answer), it's helped me decide on a solution.

Solution I've decided on:

1. I'm adding the following post-conditions to the base class Rectangle:

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

   These basically assert that Width and Height can be set independently from one another.

2. One invariant is added in the derived class Square:

   Contract.Invariant(Width == Height);
   

   This basically states just the opposite.

Taken together, these will eventually result in a contract violation — admittedly not at compile-time, but it seems that could only be done with Code Contracts in certain corner cases (namely, when a derived class starts adding pre-conditions.)

Why is the solution in the MSDN Magazine article not helpful?

The MSDN article seemingly shows a solution that has the advantage of compile-time warnings. Why do I stick with the above solution that doesn't have this bonus?

Short answer:

An unexplained change in the code examples makes it clear that the article sets up an artificial situation in order to show off Code Contracts' static analysis.

Long answer:

The article starts off with a code example (→ Figure 1) of a Rectangle class with individual setters for both Width and Height. The next time that the Rectangle class is shown (→ Figure 2), the setters have been made private and are only used through an added method SetSize(width, height).

The article does not say explain why this change was silently introduced. In fact, that change would probably not make any sense at all in the context of Rectangle alone, unless of course you already knew that you would derive a class like Square where you need to add a pre-condition width == height. You couldn't add this as a pre-condition when the setters for Width and Height are separated from one another. And if you could not add that pre-condition, you would not get a compile-time warning from Code Contracts.