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`, 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…

Accepted Answer

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 its 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));
```

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

Solution

Problem