Как я могу быть свободным в коде в инварианте объекта?

Я пытаюсь продемонстрировать инварианты в Code Contracts, и я подумал, что приведу пример отсортированного списка строк. Он поддерживает массив внутри, с запасным пространством для дополнений и т.д. - в основном как List<T>. Когда ему нужно добавить элемент, он вставляет его в массив и т.д. Я решил, что у меня есть три инварианта:

Счет должен быть разумным: неотрицательным и не более большим, чем размер буфера
Все в неиспользуемой части буфера должно быть null
Каждый элемент в используемой части буфера должен быть по крайней мере как "большой", как элемент перед ним

Теперь я попытался реализовать это следующим образом:

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

К сожалению, ccrewrite запутывает циклы.

В документации пользователя говорится, что метод должен быть просто последовательностью вызовов Contract.Invariant. Должен ли я переписать код как-то вроде этого?

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

Это несколько уродливое, хотя оно действительно работает. (Это намного лучше, чем моя предыдущая попытка, заметьте.)

Неужели мои ожидания необоснованны? Являются ли мои инварианты необоснованными?

(Также задан как вопрос в форуме Code Contracts. Я сам добавлю соответствующие ответы.)

Ответ 1

С (предварительных) страниц MSDN это выглядит как член Contract.ForAll, который может помочь вам с контрактами на 2 диапазона. Однако документация не очень ясна в отношении ее функции.

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

Ответ 2

(Я собираюсь принять ответ Хенка, но, думаю, стоит добавить это.)

Теперь на вопрос ответили форум MSDN, и результат заключается в том, что первая форма не будет работать. Инварианты действительно действительно должны быть серией вызовов Contract.Invariant, и все.

Это делает более вероятным, если статическая проверка должна понимать инвариант и обеспечивать его соблюдение.

Это ограничение можно обойти, просто поместив всю логику в другой член, например. a IsValid, а затем вызывает:

Contract.Invariant(IsValid);

Это, несомненно, испортит статическую проверку, но в некоторых случаях это может быть полезной альтернативой в некоторых случаях.

Ответ 3

Не дизайнеры немного изобретают колесо?

Что случилось с добрый старый

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

Теперь в С# у нас нет константы, но почему вы не можете просто определить функцию Invariant

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

Возможно, я пишу глупости, но даже в этом случае у него будет какая-то дидактическая ценность, когда все скажут мне неправильно.