Читать онлайн «Основы объектно-ориентированного программирования». Страница 113

В конечном итоге, выбор уровня мониторинга в производственных системах не так прост, как предполагает Хоаровское правило. Следует соблюдать несколько точных и строгих правил.

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

[x]. Если вы являетесь менеджером проекта, никогда не позволяйте своим разработчикам предполагать, что в производственной версии проверки будут включены. Заставьте каждого исходить из того, - все проверки могут быть выключены. Это особенно важно для больших систем, в природе которых устрашающие последствия ошибок.

[x]. Убедитесь, что в процессе разработки системы проверка утверждений всегда включена, по меньшей мере, на уровне предусловий.

[x]. Выполняйте интенсивное тестирование со всеми включенными проверками. Включайте также все проверки при каждом найденном жучке и устранении его последствий.

[x]. Для стандартной производственной версии решите, выберите ли версию без проверок или защищенную версию. Напомню о трех факторах, рассмотренных в самом начале этого раздела, которые следует учитывать при принятии решения.

[x]. Если вы решите выбрать версию без проверок в качестве стандарта, то включите в поставку и версию с проверками, по меньшей мере, предусловий. В случае, если система у пользователей начнет вести себя непредсказуемым способом, вопреки ожиданиям, вы сможете попросить пользователей перейти на защищенную версию, что поможет быстро отыскать неисправности системы.

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

Механизм утверждений, представленный в этой лекции, привносит несколько тонких проблем, подлежащих исследованию.

Действительно, нужно ли проверять утверждения в период выполнения? После того, как мы были в состоянии, используя утверждения, дать теоретическое определение корректности класса: каждая процедура создания должна гарантировать инвариант, и тело каждой процедуры, запущенной в состоянии, удовлетворяющем инварианту и предусловию, сохраняет в заключительном состоянии инвариант и гарантирует выполнение постусловия. Теперь мы должны выполнить математическую проверку m+n соответствующих условий (для m процедур создания и n экспортируемых процедур), и тогда долой мониторинг в период выполнения.

Мы должны, но мы не можем. Доказательство правильности программ уже многие годы является активной областью исследований, и достигло определенных успехов. Все же сегодня невозможно проверить корректность реального ПО, написанного на современных языках программирования.

Для этого необходим, в частности, и более мощный язык утверждений. Язык 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_full: 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 - функция

full: BOOLEAN is

-- Is stack full? (Заполнен ли стек?)

do

Result := (count = capacity)

ensure

full_definition: Result = (count = capacity)

end

В этом наш маленький секрет, - мы вышли из рамок исчисления высказываний, в котором булевы выражения могут строиться только из переменных, констант и знаков логических операций. Благодаря введению функций, мы получили мощный механизм, позволяющий вычислять булевы значения любым, подходящим для нас способом. Не следует беспокоиться о присутствии постусловия самой функции full, это не создает никакого пагубного зацикливания. Детали вскоре.