Search code examples
c#code-contracts

Why code contracts can be added and removed for postconditions and object invariants, but not for preconditions in C#?


Why code contracts can be added and removed for postconditions and object invariants, but not for preconditions in C#?

In the CLR via C# book I met the following excerpt:

And since a contract cannot be made stricter with new versions (without breaking compatibility), you should carefully consider preconditions when introducing a new virtual, abstract, or interface member. For postconditions and object invariants, contracts can be added and removed at will as the conditions expressed in the virtual/abstract/interface member and the conditions expressed in the overriding member are just logically AND-ed together.

That is very confusing for me that postconditions and object invariants, contracts can be added and removed at will. I would expect a suggestion that the postconditions and object invariants can become only stricter as well as the preconditions. Why am I expecting this? Because I can come up with an example where the suggestion proves wrong. E.g.

At first we had a postcondition and everything worked just fine:

using System.Diagnostics.Contracts;

public sealed class Program
{
    public static void FooBaseContract(int i) 
    {
        Contract.Ensures(i > 0);
    }
}

public class FooBase 
{
    public virtual int i 
    {
        get {return 2;} 
    }
}
public class FooDerived : FooBase
{
    public override int i 
    {
        get {return 4;} 
    }
}

Now we decide to make the postcondition stricter:

using System.Diagnostics.Contracts;

public sealed class Program
{
    public static void FooBaseContract(int i) 
    {
        Contract.Ensures(i > 4);
    }
}

public class FooBase 
{
    public virtual int i 
    {
        get {return 2;} 
    }
}
public class FooDerived : FooBase
{
    public override int i 
    {
        get {return 4;} 
    }
}

That definitely makes the code which worked with the previous postcondition incompatible with the new postcondition. That means that we lose the backward compatibility by making the postconditions stricter.

Also, I am not getting why the author refers only the virtual, abstract, or interface member. Because in the contrived example I gave above the incompatibility with the new code contract version will happen even if I change code to the following (remove all virtual, abstract, or interface member):

using System.Diagnostics.Contracts;

public sealed class Program
{
    public static void FooBaseContract(int i) 
    {
        Contract.Ensures(i > 4);
    }
}

public class FooBase 
{
    public int i 
    {
        get {return 2;} 
    }
}

So, could someone explain in a foolproof manner what am I missing here, please?

UPDATE

As was mentioned in the comments section - the code contracts is a deprecated concept. That is ok for me, I just would like to understand the idea - in this case it is why can we make the postconditions and object invariants stricter? It contradicts with my common sense, meaning that something was allowed to be returned previously (or take place for object invariants) and now we state that that something is not allowed any more and the author of the book tells that such a case is not breaking a backward compatibility.


Solution

  • The text says that the conditions are "anded" together. This means that you simply do not have the ability to remove postconditions and invariants. You can only add them regardless of how you write the code.

    Postconditions and invariants are things that must be ensured on exit. It makes sense to be able to add obligations. If you are adding a contradiction then CC should flag that as a postcondition violation.

    From a compatibility and extensibility standpoint, users of the base class will receive the guarantees they expect. They might receive additional guarantees that they don't know or care about.