Пример кодовых контрактов с ошибкой Graph.Remove (Edge e) - PullRequest
Новая
       53

Пример кодовых контрактов с ошибкой Graph.Remove (Edge e)

0 голосов
/ 02 февраля 2011

Вот простой метод манипулирования графиком, который я украсил с помощью контрактов кода.

Заявка на гарантию не будет доказана, но я не понимаю, почему!Я считаю, что он утверждает, что после вызова Remove (), либо край больше не находится в списке ребер, либо результат ложен.Он ничего не заявляет о состоянии графика, если результат верен.Статическому контролеру это не нравится, и мне не удалось, чтобы Пекс сказал мне, как (хотя я, вероятно, просто не знаю, как его использовать).

Блокировка для этого примера посторонняя, я полагаю, но я оставлю это на всякий случай.Кроме того, у делегата OnRemoveEdge нет никаких гарантий, но пока я неявно предполагаю, что он не возвращается в код Graph.Кроме того, предположение следует за ним. 

public bool Remove(E edge)
{
  Contract.Requires(edge != null);
  Contract.Ensures(!Contract.Exists(edges, e => e == edge) || !Contract.Result<bool>());

  lock (sync)
  {
    if (!OnBeforeRemoveEdge(edge)) return false;

    if (!edges.Remove(edge)) return false;
  }

  OnRemoveEdge(edge);

  Contract.Assume(!Contract.Exists(edges, e => e == edge));

  return true;
}

Обновление: я изменил код для перемещения обработчика события OnRemoveEdge () (но не делегата OnBeforeRemoveEdge) из блокировки.Но тогда, что это делает для предположения контракта, связанного с потоками?Принимает ли Code Contracts однопотоковую модель?Хммм.

1 Ответ

1 голос
/ 03 февраля 2011

Из Ответ Джека Лейтча на аналогичный вопрос :

В руководстве пользователя Кодовые контракты говорится: «Статическая проверка контракта еще не имеетквантификаторы ForAll или Exists. "

True.верно.

...