With Code Contracts, do I need to verify field/property initialization via `Ensures`?

Question

using System.Diagnostics.Contracts;

class C
{
    public C(bool x)
    {
        Contract.Ensures(this.X == x);  // is this necessary?
        this.X = x;
    }

    public readonly bool X;  // could be a property instead,
}                            // I'm just trying to keep this example simple

The point of this constructor is initializing a field, and the contract merely captures that intent. The contract has the same complexity as the code to which it applies. To me, it feels redundant, as if I had just written the same code twice (albeit from two slightly different perspectives).

Are "micro-contracts" of this kind necessary at all, or does Code Contracts infer these from the method body?

Answer 1

My opinion is yes.

If you infer contracts from the implementation any change to your implementation may change the contract. That would be like releasing an interface in version 1.0.0 and making a breaking change to it in 1.0.1 due to a simple bug fix. When you ensure to me that X = x and I am a user of your code I hope you keep your promise. Keep in mind that contract assemblies can also be distributed alongside libraries within NuGet packages for example.