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

Question

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

Answer 1

Насколько мне известно, самым мощным статическим языком DbC на данный момент является Spec # от Microsoft Research . В нем используется мощный инструмент статического анализа под названием Boogie , который, в свою очередь, использует мощный инструмент проверки теорем / ограничителей, называемый < a href = "http://Research.Microsoft.Com/projects/z3/" rel = "noreferrer"> 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

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

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

  foo(a);

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

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

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

Answer 5

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