Основы объектно-ориентированного программирования
Шрифт:
задает постусловие not empty процедуры put. Но в некоторых случаях в классе нет непосредственного двойника. Ни одно из постусловий для remove, приводимое до сих пор, не отражает аксиому
Мы, конечно, можем ввести эту аксиому неформально, добавив в постусловие комментарий, описывающий это свойство:
Подобные неформальные утверждения, синтаксически выраженные комментариями, появлялись в инвариантах цикла для maxarray и gcd.
В таких случаях два из принципиальных использований утверждений, обсуждаемых ранее, остаются применимыми, по крайней мере, частично: помощь в создании корректного продукта и его документации (утверждения, заданные комментариями, будут появляться в краткой форме класса). Другие использования, в частности отладка и тестирование, предполагают вычисление выражений, и становятся теперь неприменимыми.
Было бы предпочтительнее выражать все утверждения формально. Лучший способ достичь этой цели - расширить язык выражений, так чтобы он позволял задавать любые свойства. Это требует возможности описания сложных математических объектов - множеств, последовательностей, функций, отношений. Необходим и мощный по выразительности язык, например, язык логики предикатов первого порядка, допускающий выражения с кванторами всеобщности и существования. Существуют формальные языки спецификаций, обладающие, по крайней мере, частью такой выразительной силы. Наиболее известными являются языки Z, VDM, Larch, OBJ-2; как Z, так и VDM имеют ОО-расширения, например, Object-Z. Библиографические замечания к лекции 6 дают необходимые ссылки.
Включение полного языка спецификаций в язык этой книги полностью изменило бы ее природу. Смысл языка в том, чтобы он был простым, легким в обучении, применимым во всех программистских конструкциях. Он должен допускать быструю компиляцию и эффективную реализацию с производительностью, соизмеримой с C или Fortran.
Вместо этого, в механизме утверждений мы пошли на инженерный компромисс: он включает достаточно формальных элементов, оказывающих существенный эффект на качество ПО, но останавливается в точке убывания - границе, за которой выгоды от большей формализации, начинают оборачиваться потерями простоты и эффективности.
| Определение границы во многом определяется личным выбором. Я был удивлен, для программистского сообщества в целом эта граница не изменилась со времен первого издания этой книги. Наша деятельность требует большего формализма, но профессиональное сообщество еще не осознало этого. |
Так что пока и на ближайшее будущее утверждения остаются булевыми выражениями с некоторыми расширениями. Это не такое уж и строгое ограничение, поскольку булевы выражения допускают вызов функций.
Включение функций в утверждения
Булевы выражения не ограничиваются использованием атрибутов и локальных сущностей. Мы уже использовали возможность вызова функций в утверждениях: предусловие для put класса стек было not full, где full– функция
В этом наш маленький секрет, - мы вышли из рамок исчисления высказываний, в котором булевы выражения могут строиться только из переменных, констант и знаков логических операций. Благодаря введению функций, мы получили мощный механизм, позволяющий вычислять булевы значения любым, подходящим для нас способом. Не следует беспокоиться о присутствии постусловия самой функции full, это не создает никакого пагубного зацикливания. Детали вскоре.
Использование функций ведет к получению более абстрактных утверждений. Например, кто-то предпочтет заменить предусловие в операциях над массивом, ранее выраженное как
одним предложением в форме
с определением функции
Еще одно преимущество использования функций в выражениях в том, что они дают способ обойти ограничения выразительной силы, возникающие из-за отсутствия механизмов логики предикатов первого порядка. Неформальный инвариант нашего цикла для maxarray
формально может быть выражен так
в предположении, что slice вырабатывает нарезку - массив с индексами от lower до i, - а функция max дает максимальный элемент этого массива.