How free can I be in the code in an object invariant?

Question

I'm trying to demonstrate invariants in Code Contracts, and I thought I'd give an example of a sorted list of strings. It maintains an array internally, with spare space for additions etc - just like List<T>, basically. When it needs to add an item, it inserts it into the array, etc. I figured I had three invariants:

• The count must be sensible: non-negative and at most as big as the buffer size
• Everything in the unused part of the buffer should be null
• Each item in the used part of the buffer should be at least as "big" as the item before it

Now, I've tried to implement that in this way:

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(count >= 0 && count <= buffer.Length);
    for (int i = count; i < buffer.Length; i++)
    {
        Contract.Invariant(buffer[i] == null);
    }
    for (int i = 1; i < count; i++)
    {
        Contract.Invariant(string.Compare(buffer[i], buffer[i - 1]) >= 0);
    }
}

Unfortunately, ccrewrite is messing up the loops.

The user documentation says that the method should just be a series of calls to Contract.Invariant. Do I really have to rewrite the code as something like this?

Contract.Invariant(count >= 0 && count <= buffer.Length);
Contract.Invariant(Contract.ForAll
    (count, buffer.Length, i => buffer[i] == null));
Contract.Invariant(Contract.ForAll
    (1, count, i => string.Compare(buffer[i], buffer[i - 1]) >= 0));

That's somewhat ugly, although it does work. (It's much better than my previous attempt, mind you.)

Are my expectations unreasonable? Are my invariants unreasonable?

(Also asked as a question in the Code Contracts forum. I'll add any relevant answers here myself.)

Answer 1

From the (preliminary) MSDN pages it looks like the Contract.ForAll member could help you with the 2 range contracts. The documentation isn't very explicit about it's function though.

//untested
Contract.Invariant(Contract.ForAll(count, buffer.Length, i => buffer[i] == null));
Contract.Invariant(Contract.ForAll(1, count, 
    i => string.Compare(buffer[i], buffer[i - 1]) >= 0));

Answer 2

(I'm going to accept Henk's answer, but I think it's worth adding this.)

The question has now been answered on the MSDN forum, and the upshot is that the first form isn't expected to work. Invariants really, really need to be a series of calls to Contract.Invariant, and that's all.

This makes it more feasible for the static checker to understand the invariant and enforce it.

This restriction can be circumvented by simply putting all the logic into a different member, e.g. an IsValid property, and then calling:

Contract.Invariant(IsValid);

That would no doubt mess up the static checker, but in some cases it may be a useful alternative in some cases.

Answer 3

Aren't the designers reinventing the wheel a bit?

What was wrong with the good old

bool Invariant() const; // in C++, mimicking Eiffel

?

Now in C# we don't have const, but why can't you just define an Invariant function

private bool Invariant()
{
  // All the logic, function returns true if object is valid i.e. function
  // simply will never return false, in the absence of a bug
}
// Good old invariant in C#, no special attributes, just a function

and then just use the Code Contracts in terms of that function?

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(Invariant() == true);
}

Maybe I'm writing nonsense, but even in that case it will have some didactic value when everybody tells me wrong.