Проверка времени компиляции в Design by Contract?

Question

Я прочитал, что компилятор может принудительно использовать dbc во время компиляции. Как он это делает?

Answer 1

Насколько мне известно, самый мощный статический язык DbC на данный момент - Spec # от Microsoft Research . Он использует мощный инструмент статического анализа под названием Boogie , который, в свою очередь, использует мощный средство проверки теорем / ограничителей, называемое Z3 , для доказательства выполнения или нарушения контрактов во время разработки.

Если средство проверки теорем может доказать, что контракт будет всегда нарушаться, это ошибка компиляции. Если доказатель теоремы может доказать, что контракт никогда не будет нарушен, это оптимизация: проверки контракта удаляются из окончательной DLL.

Как указывает Чарли Мартин, проверка контрактов в целом эквивалентна решению проблемы остановки и, следовательно, невозможна. Таким образом, будет много случаев, когда доказатель теоремы не может ни доказать, ни опровергнуть договор. В этом случае выполняется проверка во время выполнения, как и в других, менее мощных системах контрактов.

Обратите внимание, что Spec # больше не разрабатывается. Механизм контрактов был извлечен в библиотеку под названием Кодовые контракты для .NET , которая будет частью .NET 4.0 / Visual Studio 2010. Однако языковая поддержка контрактов не будет.

Answer 2

Компилятор может использовать статический анализ , чтобы посмотреть на вашу программу и определить, правильно ли она работает. В качестве простого примера следующий код может попытаться получить квадратный корень из отрицательного числа (C ++):

double x;
cin >> x;
cout << sqrt(x) << endl;

Если компилятор знает, что sqrt никогда не следует вызывать с отрицательным числом, он может пометить это как проблему, поскольку он знает, что чтение из пользовательского ввода может вернуть отрицательное число. С другой стороны, если вы сделаете это:

double x;
cin >> x;
if (x >= 0) {
    cout << sqrt(x) << endl;
} else {
    cout << "Can't take square root of negative number" << endl;
}

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

Answer 3

Проектирование по контракту является очень абстрактным термином, поскольку может быть много спецификационных формализмов с различной степенью выраженности. Кроме того, в настоящее время существует предел возможностей статического анализа для проверки и обеспечения выполнения спецификаций. Это одна из самых активных академических и промышленных областей исследований в области компьютерных наук.

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

В целом, статический анализ пытается построить модель контракта и модель реальной программы и сравнить их. Например, если контракт не позволяет вам вызывать функцию, когда объект находится в состоянии S, он попытается определить, в какой последовательности вызовов вы могли бы оказаться в состоянии S.

Answer 4

Некоторые языки, такие как D , имеют достаточно мощное свертывание постоянной времени компиляции и проверку условий времени компиляции (для D static assert(boolCond, msg);, IIRC C / C ++ может использовать #if и pragma или #error)

Answer 5

Какой компилятор и на каком языке? Эйфель может сделать это до некоторой степени. Но помните, что полное обеспечение разработки по контракту означало бы возможность решить проблему остановки (доказательство: предположим, что у вас есть компилятор, который может это сделать. Тогда компилятор должен будет иметь возможность идентифицировать произвольную функцию с истинным условием выхода который не может выполнить условие выхода из-за бесконечного цикла или бесконечной рекурсии. Таким образом, он сводится к остановке.

Обычно это означает, что если у вас есть звонок

  foo(a);

и где-то еще определить

  function foo(a:int) is
     assert 0 < a && a < 128
     ...
  end

тогда компилятор может проверить, что a фактически находится в открытом интервале (0..128).