Code Contracts and Inheritance(Precondition on overridden method)

Question

Currently code contracts do not allow preconditions on members in derived classes where the member already has a precondition set in the base class(I actually currently get a warning and not an error). I do not understand the logic behind this. I understand that it has to do with Liskov's substitution rule stating that a derived class should always be able to be used in places where the parent is expected. Of course "used" means work as expected. This seems okay to me for interfaces as the different types implementing an interface don't add state and hence can oblige the contract exactly. However, when you inherit from a base class, you are doing so to add state and special functionality and more often than not the overriding method would have extra requirements. Why can't preconditions be ANDed together just like post conditions and object invariants?

Take a look below:

class Speaker
{
    public bool IsPlugged { get; set; }
    protected virtual void Beep()
    {
        Contract.Requires(IsPlugged);
        Console.WriteLine("Beep");
    }
}

class WirelessSpeaker : Speaker
{
    public bool TransmitterIsOn { get; set; }
    protected override void Beep()
    {
        Contract.Requires(TransmitterIsOn);
        base.Beep();
    }
}

You may argue that this class hierarchy breaks Liskov's rule because the wireless speaker may not be able to beep when passed to methods that expect a Speaker. But isn't that why we use code contracts? to make sure that the requirements are met?

Answer 1

Code contracts are not about the meeting of the requirements, but their communication. Callers of Speaker.Beep are bound by a contract that only takes effect in some cases.

WirelessSpeaker narrows the functional space of Speaker - that's where Liskov comes into play. I can only use that particular Speaker effectively if I know it's wireless. In that case, I should explicitly accept WirelessSpeaker, not Speaker, and avoid the substitution issues.

Edit in response to comments:

The author of WirelessSpeaker chooses how to interpret the Beep command. Choosing a new contract, visible at this level but not at the base level, imposes constraints that apply <100% of the time when using Speakers.

If it were to simply not beep when the transmitter isn't on, we wouldn't be talking about Code Contracts. Their intention is not to communicate at runtime, but at design time, the semantics of the call (not just its syntax).

The fact that an exception occurs at runtime, ultimately preventing the "incorrect" call, is largely irrelevant here.