[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);
    }
}

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

//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));

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

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

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

Contract.Invariant(IsValid);