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

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

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

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

[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. Я сам добавлю здесь любые соответствующие ответы.)

Источник

3 ответа

Решение

На (предварительных) страницах 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));
Источник

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

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

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

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

Contract.Invariant(IsValid);

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

Источник

Разве дизайнеры не изобретают велосипед немного?

Что было не так со старым добрым

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

?

Теперь в C# у нас нет const, но почему вы не можете просто определить 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);
}

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

Источник
Другие вопросы по тегам