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

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

25 голосов
/ 31 июля 2009

Я пытаюсь продемонстрировать инварианты в контрактах кода, и я подумал, что приведу пример отсортированного списка строк. Он поддерживает массив внутри, с запасным пространством для дополнений и т. Д. - как и 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 ]

8 голосов
/ 31 июля 2009

На (предварительных) страницах 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));
3 голосов
/ 31 июля 2009

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

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

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

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

Contract.Invariant(IsValid);

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

1 голос
/ 24 августа 2009

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

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

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

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

...