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?

a bit similar to http://stackoverflow.com/questions/2767247/design-by-contracts-and-constructors — hatchet - done with SOverflow, Aug 16 '13 at 13:40
In your example, it does seem redundant since it's so trivial an example. But in general, I don't see the harm in consistent Ensuring. What if the parameter was `int capacity`, but you Ensure that `Size == capacity`? That is a little less obvious. Where do you draw the line on what's trivial/obvious/unneeded? Will the reader understand and agree? — hatchet - done with SOverflow, Aug 16 '13 at 13:48
@hatchet: Re: _"What if…?"_ Then as far as I am concerned, that would be a different question. I chose that specific code example intentionally. _"Where do you draw the line on what's trivial…?"_ That's a good question. And I have no answer to it, since Code Contracts draws that line, not me. Thus my question whether my trivially-seeming code example *is* trivial to Code Contracts. — stakx - no longer contributing, Aug 16 '13 at 20:26
Aside from the question of static analysis, the problem I see is that routinely skipping the 'trivial' cases invites users of the code to poke inside the internals of the code to determine which of these cases is the reason you've omitted what would be an obvious Ensures: 1) you could Ensure it but considered it trivial, 2) you can't Ensure it, for a non-obvious (to outsiders) reason. — hatchet - done with SOverflow, Aug 16 '13 at 21:51

score 2 · Accepted Answer · answered Aug 22 '13 at 18:41

2

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.

answered Aug 22 '13 at 18:41

Dandy

272
3
11

1

Contracts are by definition "redundant" with the code. That's the enitre premise of Contracts, something you can check against the code. If there is no redundancy, then there is nothing to check. – Manuel Fahndrich Aug 27 '13 at 17:46

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

1 Answers1