Мы должны, но мы не можем. Доказательство правильности программ уже многие годы является активной областью исследований, и достигло определенных успехов. Все же сегодня невозможно проверить корректность реального ПО, написанного на современных языках программирования.
| Для этого необходим, в частности, и более мощный язык утверждений. Язык IFL, обсуждаемый ниже, может быть использован как часть стратегии многоярусного доказательства. |
Даже, если со временем методы и инструментальные средства доказательства станут доступными, можно ожидать, что отказаться от мониторинга не удастся. В системе всегда останется место трудно предсказуемым событиям - ошибкам аппаратуры, ошибкам в самом доказательстве. Поэтому следует применять хорошо известную в инженерии технику - множественные, независимые способы проверки.
Выразительная сила утверждений
Как можно было заметить, применяемый язык утверждений является языком обычных булевых выражений, обогащенный несколькими понятиями, такими как old. Как результат, он ограничен и не позволяет включить в наши классы некоторые свойства, достаточно просто выражаемые в математической нотации, используемой при описании АТД.
Утверждения класса стек дают хороший пример того, что выразимо, и что не выразимо в нашем языке. Мы найдем, что многие аксиомы и предусловия из спецификации АТД, приведенной в лекции 6, прямым образом отображаются в утверждения класса. Например, аксиома
A4. not empty (put (s, x))
задает постусловие not empty процедуры put. Но в некоторых случаях в классе нет непосредственного двойника. Ни одно из постусловий для remove, приводимое до сих пор, не отражает аксиому
A2. remove (put (s, x)) = s
Мы, конечно, можем ввести эту аксиому неформально, добавив в постусловие комментарий, описывающий это свойство:
remove is
-- Удалить элемент вершины
require
not_empty: not empty -- i.e. count > 0
do
count := count - 1
ensure
not_fulclass="underline" not full
one_fewer: count = old count - 1
LIFO_policy: -- item является последним элементом, помещенным в стек
-- и еще не удален, если таковое имело место.
End
Подобные неформальные утверждения, синтаксически выраженные комментариями, появлялись в инвариантах цикла для maxarray и gcd.
В таких случаях два из принципиальных использований утверждений, обсуждаемых ранее, остаются применимыми, по крайней мере, частично: помощь в создании корректного продукта и его документации (утверждения, заданные комментариями, будут появляться в краткой форме класса). Другие использования, в частности отладка и тестирование, предполагают вычисление выражений, и становятся теперь неприменимыми.
Было бы предпочтительнее выражать все утверждения формально. Лучший способ достичь этой цели - расширить язык выражений, так чтобы он позволял задавать любые свойства. Это требует возможности описания сложных математических объектов - множеств, последовательностей, функций, отношений. Необходим и мощный по выразительности язык, например, язык логики предикатов первого порядка, допускающий выражения с кванторами всеобщности и существования. Существуют формальные языки спецификаций, обладающие, по крайней мере, частью такой выразительной силы. Наиболее известными являются языки Z, VDM, Larch, OBJ-2; как Z, так и VDM имеют ОО-расширения, например, Object-Z. Библиографические замечания к лекции 6 дают необходимые ссылки.
Включение полного языка спецификаций в язык этой книги полностью изменило бы ее природу. Смысл языка в том, чтобы он был простым, легким в обучении, применимым во всех программистских конструкциях. Он должен допускать быструю компиляцию и эффективную реализацию с производительностью, соизмеримой с C или Fortran.
Вместо этого, в механизме утверждений мы пошли на инженерный компромисс: он включает достаточно формальных элементов, оказывающих существенный эффект на качество ПО, но останавливается в точке убывания - границе, за которой выгоды от большей формализации, начинают оборачиваться потерями простоты и эффективности.
| Определение границы во многом определяется личным выбором. Я был удивлен, для программистского сообщества в целом эта граница не изменилась со времен первого издания этой книги. Наша деятельность требует большего формализма, но профессиональное сообщество еще не осознало этого. |
Так что пока и на ближайшее будущее утверждения остаются булевыми выражениями с некоторыми расширениями. Это не такое уж и строгое ограничение, поскольку булевы выражения допускают вызов функций.
Включение функций в утверждения
Булевы выражения не ограничиваются использованием атрибутов и локальных сущностей. Мы уже использовали возможность вызова функций в утверждениях: предусловие для put класса стек было not full, где full - функция
fulclass="underline" BOOLEAN is
-- Is stack full? (Заполнен ли стек?)
do
Result := (count = capacity)
ensure
full_definition: Result = (count = capacity)
end
В этом наш маленький секрет, - мы вышли из рамок исчисления высказываний, в котором булевы выражения могут строиться только из переменных, констант и знаков логических операций. Благодаря введению функций, мы получили мощный механизм, позволяющий вычислять булевы значения любым, подходящим для нас способом. Не следует беспокоиться о присутствии постусловия самой функции full, это не создает никакого пагубного зацикливания. Детали вскоре.
Использование функций ведет к получению более абстрактных утверждений. Например, кто-то предпочтет заменить предусловие в операциях над массивом, ранее выраженное как
index_not_too_smalclass="underline" lower <= i
index_not_too_large: i <= upper
одним предложением в форме
index_in_bounds: correct_index (i)
с определением функции
correct_index (i: INTEGER): BOOLEAN is
-- Является ли i внутри границ массива?
do
Result := (i >= lower) and (i <= upper)
ensure
definition: Result = ((i >= lower) and (i <= upper))
end
Еще одно преимущество использования функций в выражениях в том, что они дают способ обойти ограничения выразительной силы, возникающие из-за отсутствия механизмов логики предикатов первого порядка. Неформальный инвариант нашего цикла для maxarray
-- Result является максимумом нарезки массива t в интервале [t.lower,i]
формально может быть выражен так