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

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

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

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

Технические приемы, введенные в предыдущих лекциях, были направлены на создание надежного ПО. Дадим их краткий обзор - было бы бесполезно рассматривать более продвинутые концепции до приведения в порядок основных механизмов надежности. Первым и определяющим свойством объектной технологии является почти навязываемая структура программной системы - простая, модульная, расширяемая, - проще гарантирующая надежность, чем в случае "кривых" структур, возникающих при применении ранних методов разработки. В частности, усилия по ограничению межмодульного взаимодействия, сведения его к минимуму, были в центре дискуссии о модульности. Результатом стал запрет общих рисков, снижающих надежность, - отказ от глобальных переменных, механизм ограниченного взаимодействия модулей, отношения наследования и вложенности. Общее наблюдение: самый большой враг надежности (и качества ПО в целом) - это сложность. Создавая наши структуры настолько простыми, сколь это возможно, мы достигаем необходимого, но не достаточного условия, гарантирующего надежность. Прежнее обсуждение служит лишь верной отправной точкой в последующих систематических усилиях.

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

Еще одно необходимое оружие - автоматическое управление памятью, в особенности сборка мусора. В лекции, посвященной этой теме, в деталях пояснено, почему для любой системы, оперирующей динамическими структурами данных, столь опасно опираться на управление этим процессом вручную. Сборка мусора не роскошь - это ключевой компонент ОО-среды, обеспечивающий надежность.

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

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

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

Предположим, некто пришел к вам с программой из 300 000 строк на С и спрашивает, корректна ли она? Если вы консультант, то взыщите высокую плату и ответьте - "нет". Вы, вероятно, окажетесь правы.

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

x:= y+1

сам по себе не является ни корректным, ни не корректным. Эти понятия приобретают смысл лишь по отношению к ожидаемому эффекту присваивания. Например, присваивание корректно по отношению к утверждению: "Переменные x и y имеют различные значения". Но не гарантируется его корректность по отношению к высказыванию: "переменная x отрицательна", поскольку результат присваивания зависит от значения y, которое может быть положительным.

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

Свойство корректности ПО

Корректность - понятие относительное.

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

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

[x]. Значительно лучшее понимание проблемы и достижение ее решения.

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

[x]. Обеспечение основ для систематического тестирования и отладки.

Оставшаяся часть лекции посвящена исследованию этих вопросов. Одно предупреждение: языки программирования С, С++ и другие имеют оператор утверждения assert, динамически проверяющий истинность заданного утверждения в момент выполнения программы и останавливающий вычисление, если утверждение является ложным. Эта концепция, хотя и имеет отношение к предмету обсуждения, но является лишь малой частью использования утверждений в ОО-методе. Потому, если подобно многим разработчикам вы знакомы с этим оператором, не обобщайте ваше знание на всю картину, почти все концепции этой лекции, возможно, будут новыми.

От неформальных высказываний перейдем к простой математической нотации, принятой в теории формальной проверки правильности программ и имеющей ценность при доказательстве корректности программных элементов.

Пусть А - это некоторая операция (оператор или тело программы). Формула корректности (correctness formula) - это выражение в форме:

{P} A {Q}

Формула выражает свойство, которое может быть или не быть истинным:

Смысл формулы корректности {P} A {Q}

Любое выполнение А, начинающееся в состоянии, где P истинно, завершится и в заключительном состоянии будет истинно Q.

Формула корректности, называемая также триадой Хоара, - математическое понятие, а не программистская конструкция. Она не является частью языка программирования и введена для того, чтобы выражать свойства программных элементов. В этой формуле А, как было сказано, обозначает операцию, P и Q - свойства вовлекаемых в рассмотрение сущностей, называемые утверждениями (точный смысл этого термина будет определен ниже). Утверждение P называется предусловием, а Q - постусловием.

С этого момента обсуждение корректности ПО будет связываться не с программным элементом А, а с триадой, содержащей этот элемент А, предусловие P и постусловие Q. Единственной целью становится установление того, что триада Хоара {P} A {Q} выполняется (истинна).

Вот пример выполняемой тривиальной формулы, в которой полагается, что x имеет тип integer:

{x>=9} x:= x+5 {x>=13}

Понятия "сильнее" и "слабее" пришли из логики. Говорят, что P1 сильнее, чем P2, а P2 слабее, чем P1, если P1 влечет P2 и они не эквивалентны. Каждое утверждение влечет True, и из False следует все что угодно. Можно говорить, что True является слабейшим, а False сильнейшим из всех возможных утверждений.

Давайте взглянем на формулу корректности с позиций человека, собирающегося наняться на работу по выполнению операции А. Каковы с его точки зрения наилучшие предусловие P и постусловие Q, если у него есть возможность выбора? Возможность усиления предусловия означает, что можно предъявлять более жесткие требования к работодателю, что можно уменьшить число ситуаций, в которых следует приступать к выполнению работы. Так что сильное предусловие это "хорошие новости" для работника. Наилучшей для него работой - синекурой является работа, чья спецификация выражается формулой:

Синекура 1

{False} A {...}

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

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

Синекура 2

{...} A {True}

Как бы не была выполнена работа, постусловие в этом случае будет истинным по определению. Кстати, почему эта работа является все-таки второй по предпочтительности? Причина, как можно видеть из определения триады Хоара, в завершаемости (terminate). Определение устанавливает, что выполнение должно завершиться в состоянии, удовлетворяющем Q, всякий раз, когда оно начинается в состоянии, удовлетворяющем P. Для синекуры 1, где нет состояний, удовлетворяющих P, не имеет значения, что делает А даже если программный текст приводит к выполнению бесконечного цикла, или ломает компьютер. Любое А будет корректным по отношению к данной спецификации. Для синекуры 2, однако, требуется завершение работы, должно существовать заключительное состояние, не важно, что делает А, но то, что делается, должно быть выполнено за конечное время.

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

Как только корректность ПО определена как согласованность реализации с ее спецификацией, следует предпринять шаги по включению спецификации в сам программный продукт. Для большинства в программистском сообществе это все еще новая идея. Привычно писать программы, устанавливая тем самым, - как делать (the how); менее привычно рассматривать описание целей - что делать (the what) - как часть программного продукта.

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

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

Синтаксически утверждения в нашей нотации будут обычными булевыми выражениями с небольшими расширениями. Одним из расширений является введение в нотацию термина "old", другим - введение символа ";" для обозначения конъюнкции (логического И). Вот пример:

n>0; x /= Void

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

Positive: n > 0

Not_void: x /= Void

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

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

Этот пример даст возможность ознакомиться с практическим использованием утверждений. В предыдущей лекции была дана схема параметризованного класса "стек" в форме:

class STACK [G] feature

... Объявление компонент:

count, empty, full, put, remove, item

end

Реализация появится ниже. До рассмотрения проблем реализации важно отметить, что программы характеризуются строгими семантическими свойствами, не зависящими от специфики реализации. Например:

[x]. Программы remove и item применимы, только если число элементов стека не равно нулю.

[x]. put увеличивает, remove - уменьшает число элементов на единицу.

Такие свойства являются частью спецификации АТД, и даже люди далекие от использования любых формальных подходов неявно их понимают. Но в общих подходах к разработке ПО в программных текстах нельзя обнаружить следов спецификации. Предусловие и постусловие программы можно сделать явными элементами ПО. Так и поступим. Введем предусловие и постусловие как специальный вид объявлений с помощью ключевых слов require и ensure соответственно. Для класса "стек" это приведет к следующей записи, где временно оставлены пустые места для реализации:

indexing

description: "Стеки: Структуры с политикой доступа Last-In, First-Out %

%Последний пришел - Первый ушел"

class STACK1 [G] feature - Access (Доступ)

count: INTEGER

-- Число элементов стека

item: G is

-- Элемент вершины стека

require

not empty

do

...

end

feature - Status report (Отчет о статусе)

empty: BOOLEAN is

-- Пуст ли стек?

do ... end

full: BOOLEAN is

-- Заполнен ли стек?

do

...

end

feature - Element change (Изменение элементов)

put (x: G) is

-- Добавить элемент x на вершину.

require

not full

do

...

ensure

not empty

item = x

count = old count + 1

end

remove is

-- Удалить элемент вершины.

require

not empty

do

...

ensure

not full

count = old count - 1

end

end

Оба предложения require и ensure являются возможными; когда они присутствуют, то появляются в фиксированных местах, require - перед предложением local.

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

[x]. put не может быть вызвана, если стек заполнен;

[x]. remove и item не могут быть применены к пустому стеку.

Предусловия применяются ко всем вызовам программы, как внутри класса, так и у клиента. Корректная система никогда не вызовет программу в состоянии, в котором не выполняется ее предусловие.

Постусловие выражает свойство состояния, завершающего выполнение программы. Здесь:

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

[x]. После remove стек не может быть полон, число его элементов на единицу уменьшилось.

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

В постусловиях доступна специальная нотация old. Она используется, например, в программах remove и item для выражения изменения значения count. Запись old e, где e - выражение (в большинстве случаев - атрибут) обозначает значение, которое данное выражение имело на входе программы. Любое вхождение e, которому не предшествует old, означает значение выражения на выходе программы.

Постусловие программы put включает предложение:

count = old count + 1

устанавливающее, что put, примененное к любому объекту, должно увеличить на единицу значения поля count этого объекта.

Понятно ваше нетерпение и желание незамедлительно узнать, каков же эффект от утверждений при выполнении программы; что произойдет при вызове put при заполненном стеке, или что будет, когда empty дает true по завершении вызова put? Полный ответ на этот вопрос дать еще слишком рано, но предварительный использует любимое словечко адвокатов - это зависит (it depends).

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

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

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

Все это учитывается в следующих разделах, являясь методологическим вкладом утверждений и метода Проектирование по Контракту - концептуального средства анализа, проектирования, реализации и документирования, помогающего нам построить ПО со встроенной надежностью (reliability is built-in), в терминологии Миллса строить корректную программу и знать это.

Предусловие и постусловие программы определяют контракт со всеми ее клиентами.

Связывая с программой r предложения require pre и ensure post, класс говорит своим клиентам:

"Если вы обещаете вызвать r в состоянии, удовлетворяющем pre, то я обещаю в заключительном состоянии выполнить post".

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

[x]. Предусловие связывает клиента: определяются условия, при которых вызов программы клиентом легитимен. Обязательства клиента приносят пользу поставщику.

[x]. Постусловие связывает класс: программа обязана обеспечить условия по ее завершению. Здесь польза клиента оборачивается обязательствами поставщика класса.

Вот пример контракта для одной из программ нашего примера:

Таблица 11.1.Контракт программы: программа put класса стек

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

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

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

sqrt (x: REAL): REAL is

-- Квадратный корень из x

require

x >= 0

do ... end

можно смело применять алгоритм, не учитывающий случай отрицательного x, поскольку это предусмотрено предусловием, и ответственность за его выполнение несут клиенты программы. С первого взгляда это может показаться опасным, но читайте дальше. Фактически метод Проектирования по Контракту идет дальше. Предположим, что мы написали в предложении do предыдущей программы следующий текст:

if x < 0 then

"Обработать ошибку как-нибудь"

else

"Выполнить нормальное вычисление квадратного корня"

end

Заметьте, в этом не только нет никакой необходимости, но это и неприемлемо! Этот факт можно отразить в следующем методологическом правиле:

Принцип Нет-Избыточности

Ни при каких обстоятельствах в теле программы не должно проверяться ее предусловие

Это правило противоречит тому, чему учат во многих учебниках по программированию, где необходимость проверок часто выступает под знаменами "защитного программирования" (defensive programming). Его идея в том, что для получения надежного ПО каждая программа должна защищать себя настолько, насколько это возможно. Лучше больше проверок, чем недостаточно; нельзя доверять незнакомцам; еще одна проверка может и не поможет, но и не навредит делу.

Проектирование по контракту утверждает противное: избыточные проверки могут нанести вред. Конечно, это кажется странным, на первый взгляд. Это естественная реакция, полагать, что дополнительная проверка в худшем случае может быть бесполезной, но не может быть причиной неполадок. Возьмем, например, программу sqrt, включившую проверку x<0, хотя ее клиенты были проинструктированы о необходимости обеспечения x>=0. Что в этом плохого? С микроскопической точки зрения, ограничив наше видение узким мирком sqrt, кажется, что включение проверки делает программу более устойчивой. Но мир системы не ограничивается одной программой - он содержит множество программ в множестве классов. Для получения надежной системы необходимо перейти к макроскопическому видению проблемы, обобщающему всю архитектуру.

С этой глобальной точки зрения простота становится критическим фактором. Сложность - главный враг качества. Когда в этот концерн привносятся излишние проверки, то это уже не покажется столь безобидным делом. Экстраполируйте на тысячи программ в системе среднего размера (или на десятки и сотни тысяч в большой системе) проверку (if x<0 then ...), столь безобидную с первого взгляда, - все это начнет выглядеть подобно монстру бесполезной сложности. Добавляя избыточные проверки, добавляете больше кода. Больше кода - больше сложности, отсюда и больше источников условий, приводящих к тому, что все пойдет не так, это приведет к дальнейшему разрастанию кода и так до бесконечности. Если пойти по этой дороге, то определенно можно сказать одно - мы никогда не достигнем надежности. Чем больше пишем, тем больше придется писать.

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

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

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

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

require

input > 0

хотя и желательно, но технически не реализуемо. Полагаться на пользователя в контрактах нельзя. В данной ситуации нет заменителя обычной конструкции проверки условия, включая почтенный if - then - else; полезен и механизм обработки исключений.

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

Рис. 11.1.  Использование модулей - фильтров

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

Еще одно типичное заблуждение - рассматривать утверждения как управляющую структуру, реализующую разбор случаев. К этому моменту должно быть ясно, что не в этом их роль. Если написать программу sqrt, в которой отрицательные значения будут обрабатываться одним способом, а положительные - другим, то писать предусловие - предложение require не следует. В этом случае используется обычный разбор случаев: оператор if - then - else, или оператор case языка Pascal, или оператор inspect, введенный в этой книге как раз для таких целей.

Утверждения выражают нечто иное. Они говорят о корректности условий. Если sqrt имеет предусловие, то вызов, в котором x<0, это "жучок" (bug).

Правило нарушения утверждения (1)

Нарушение утверждения в период выполнения является проявлением "жучка" в ПО.

Слово "жучок" не принадлежит к научному лексикону, но этот термин понятен всем программистам. Учитывая контракты, это правило можно уточнить:

Правило нарушения утверждения (2)

Нарушение предусловия является проявлением "жучка" у клиента.

Нарушение постусловия является проявлением "жучка" у поставщика.

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

Нарушение постусловия означает, что программа, предположительно вызванная в корректных условиях, не выполнила свою часть работы, предусмотренную контрактом. Здесь тоже ясно, кто виноват, а кто нет: "жучок" в программе, клиент не виновен.

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

Термины, обозначающие бедствия ПО

Ошибка (Error) - неверное решение, принятое при разработке программной системы.

Дефект (Defect) - свойство программной системы, которое может стать причиной отклонения системы от намеченного поведения.

Неисправность (Fault) - событие в программной системе, приведшее к отклонению от нормального поведения в процессе одного из запусков системы.

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

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

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

Поставляемый с утверждениями класс STACK был оставлен пока в схематичной форме (STACK1). Теперь на суд предстанет полная версия, включающая реализацию.

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

Рис. 11.2.  Реализация стека на базе массива

Массив, названный representation, имеет границы 1 и capacity: реализация использует также целочисленный атрибут count, отмечающий вершину стека. Заметьте, после того, как мы откроем для себя наследование, появится возможность писать классы с отложенной реализацией, что позволит покрывать несколько возможных реализаций, а не одну конкретную. Даже для класса c фиксированной реализацией, например, как здесь на базе массива, мы будем иметь возможность строить его как потомка родительского класса Array. В данный момент никакие методы наследования применяться не будут.

Вот он класс. Остается напомнить, что для массива a операция, присваивающая значение x его i-му элементу, записывается так: a.put(x,i). Получить i-й элемент можно так: a.item(i) или a @ i. Если, как здесь, границы заданы, то i во всех случаях лежит между этими границами: 1<= i <= capacity.

indexing

description: "Стеки: Структуры с политикой доступа Last-In, First-Out %

% Последний пришел - Первый ушел, и с фиксированной емкостью"

class STACK2 [G] creation

make

feature - Initialization (Инициализация)

make (n: INTEGER) is

-- Создать стек, содержащий максимум n элементов

require

positive_capacity: n >= 0

do

capacity := n

create representationlmake (1, capacity)

ensure

capacity_set: capacity = n

array_allocated: representation /= Void

stack_empty: empty

end

feature - Access (Доступ)

capacity: INTEGER

-- Максимальное число элементов стека

count: INTEGER

-- Число элементов стека

item: G is

-- Элемент на вершине стека

require

not_empty: not empty -- i.e. count > 0

do

Result := representation @ count

end

feature -- Status report (Отчет о статусе)

empty: BOOLEAN is

-- Пуст ли стек?

do

Result := (count = 0)

ensure

empty_definition: Result = (count = 0)

end

full: BOOLEAN is

-- Заполнен ли стек?

do

Result := (count = capacity)

ensure

full_definition: Result = (count = capacity)

end

feature -- Element change (Изменение элементов)

put (x: G) is

-- Добавить элемент x на вершину

require

not_full: not full -- т.е. count < capacity в этом представлении

do

count := count + 1

representation.put (count, x)

ensure

not_empty: not empty

added_to_top: item = x

one_more_item: count = old count + 1

in_top_array_entry: representation @ count = x

end

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

end

feature {NONE} -- Implementation (Реализация)

representation: ARRAY [G]

-- Массив, используемый для хранения элементов стека

invariant

... Будет добавлен позднее ...

end

Текст класса иллюстрирует простоту работы с утверждениями. Это полный текст, за исключением предложений invariant, задающих инварианты класса, которые будут добавлены позднее в этой лекции. Давайте исследуем различные свойства класса.

Это первый законченный класс этой лекции, не слишком далеко отличающийся от того, что можно найти в профессиональных библиотеках повторно используемых ОО-компонентов, таких как Базовые библиотеки. Одно замечание о структуре класса. Поскольку класс имеет более двух-трех компонентов, возникает необходимость сгруппировать его компоненты подходящим образом. Нотация позволяет реализовать такую возможность введением множества предложений feature. Это свойство группировки компонентов, введенное в предыдущей лекции, использовалось там, как способ задания различного статуса экспорта компонентов. И здесь в последней части класса, помеченной Implementation, это свойство используется для указания защищенности компонента representation. Но преимущества группирования можно использовать и при неизменном статусе экспорта. Его цель - сделать класс простым при чтении и легче управляемым, группируя компоненты по категориям. После каждого ключевого слова feature появляется комментарий, называемый комментарий к предложению Feature (Feature Clause Comment). Он позволяет дать содержательное описание данной категории - роль компонентов, включенных в этот раздел. Категории, используемые в примере, те же, что и при описании класса STACK1 с добавлением раздела Initialization с процедурой создания (конструктором).

Стандартные категории feature и связанные с ними комментарии к предложениям Feature являются частью общих правил организации повторно используемых библиотек классов.

Утверждения из STACK2 иллюстрируют фундаментальную концепцию - разницу между императивным и аппликативным видением.

Утверждения empty и full могут вызвать удивление. Приведу еще раз текст full:

full: BOOLEAN is

-- Заполнен ли стек?

do

Result := (count = capacity)

ensure

full_definition: Result = (count = capacity)

end

Постусловие говорит, что Result имеет значение выражения (count = capacity). Но оператор присваивания именно это значение присваивает переменой Result. В чем же смысл написания постусловия? Не является ли оно избыточным?

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

Инструкция предписывает (prescriptive), утверждение описывает (descriptive). Инструкция описывает "как", утверждение описывает "что". Инструкция является частью реализации, утверждение - элементом спецификации.

Инструкция императивна, утверждение - аппликативно. Эти два термина выражают фундаментальную разницу между программированием и математикой.

[x]. Компьютерные операции могут изменять состояние аппаратно-программной машины. Инструкции в языках программирования являются командами (императивные конструкции), заставляющие машину выполнять такие операции.

[x]. Математические вычисления никогда ничего не меняют. Как отмечалось при рассмотрении АТД, взятие квадратного корня от числа 2 не меняет это число. Вместо этого математики описывают как, используя свойства одних объектов, вывести свойства других, таких как v2, полученных применением (applying - отсюда и термин "аппликативный") математических трансформаций.

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

Причина близости нотаций в том, что присваивание зачастую кратчайший путь достижения эквивалентности. Но при переходе к более сложным примерам концептуальное различие между спецификацией и реализацией будет только возрастать. Даже в простейшем случае вычисления квадратного корня постусловие может быть задано в форме: abs(Result^2 -x) <= tolerance, где abs - обозначает абсолютное значение, а tolerance - допустимое отклонение от точного значения. Инструкции, вычисляющие квадратный корень, могут быть не тривиальными, реализуя определенный алгоритм вычисления квадратного корня.

Даже для put в классе STACK2 одной и той же спецификации могут соответствовать различные алгоритмы, например:

if count = capacity then Result := True else Result := False end

или упрощенный вариант, учитывающий правила инициализации:

if count = capacity then Result := True end

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

Предупреждение: по практическим соображениям допускается включение в утверждение функций - по внешнему виду императивных элементов. Эта проблема исследуется в конце этой лекции.

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

Таблица 11.2.Императивно - аппликативное противопоставление

Предусловие в процедуре создания (конструкторе) make класса STACK1 требует комментария. Оно устанавливает n>=0 и, следовательно, допускает пустые стеки. Если n=0, то make вызовет процедуру создания для массивов, также имеющую имя make, с аргументами 1 и 0 для нижней и верхней границ соответственно. Это не ошибка, это соответствует спецификации процедуры создания массивов, которая в случае, когда нижняя граница на единицу больше верхней, создает пустой массив.

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

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

Центральная идея Проектирования по контракту выражена в принципе Нет_Избыточности, суть которого в том, что за выполнение условия, необходимого для правильного функционирования программы, должен нести ответственность только один из партнеров контракта.

Какой же? В каждом случае есть две возможности.

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

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

Первую ситуацию назовем требовательной (demanding), вторую - толерантной (tolerant). Класс STACK2 иллюстрирует требовательный стиль, толерантная версия, не содержащая предусловий, может выглядеть так:

remove is

-- Удалить элемент вершины стека

do

if empty then

print ("Ошибка: попытка удаления элемента из пустого стека")

else

count := count - 1

end

end

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

Рис. 11.3.  Реклама толерантного стиля

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

Исследуем эту проблему чуть глубже. Условие корректности описывает требования, необходимые для успешной работы программы. Толерантная версия программы remove является хорошим примером, демонстрирующим слабости этого стиля. Действительно, что может сделать бедная, занимающаяся выталкиванием программа, когда стек пуст? Она делает храбрую попытку выдать явно неинформативное сообщение об ошибке, но на большее она не способна - ей недоступен контекст клиента, она не способна определить, что нужно делать, когда стек пуст. Только клиент - модуль, использующий стек для своих целей, например, модуль разбора текста в компиляторе, - обладает достаточной информацией для принятия нужного решения. Является ли это нормальным, хотя и бесполезным запросом, который следует просто проигнорировать. Если это ошибка, как следует ее обработать: выбросить ли исключение, попытаться скорректировать ситуацию, или, в крайнем случае, выдать информативное для пользователя сообщение об ошибке.

Обсуждая пример с квадратным корнем, приводился такой вариант программы:

if x < 0 then

"Обработайте ошибку как-нибудь"

else

"Выполнить нормальное вычисление квадратного корня"

end

Ключевое слово здесь "как-нибудь". Предложение then скорее заклинание, чем программный код: нет разумной, общецелевой техники обработки случая x<0. Только автор клиента может знать, что значит этот случай - ошибка в ПО, возможность замены нулевым значением, причина для возбуждения исключения...

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

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

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

Принцип обоснованности предусловия

Каждое предусловие программы при требовательном стиле проектирования должно удовлетворять следующим требованиям:

1 Предусловие появляется в официальной документации, поставляемой авторам клиентских модулей.

2 Предусловие формулируется только в терминах спецификации, что делает возможным его вычисление.

Первое требование поддерживается понятием краткой формы, изучаемой позднее в этой лекции. Второе требование исключает появление ограничений, определяемых реализацией поставщика программы. Например, для программы, занимающейся выталкиванием элементов из стека, предусловие not empty является требованием, проверяемым в терминах спецификации, и вытекающим из очевидного факта - из пустого стека ничего нельзя вытолкнуть. При вычислении квадратного корня предусловие x>0 отражает известный математический факт, - отрицательные числа не имеют вещественных квадратных корней.

Некоторые ограничения могут навязываться реализацией. Например, в программе put из класса STACK2 присутствие в качестве предусловия require not full связано с реализацией стека на основе массива. Но это не является нарушением принципа, поскольку класс STACK2 в полном соответствии с его спецификацией определяет стеки ограниченной емкости, что отражено, например, в предложении indexing этого класса. АТД, служащий в роли спецификации этого класса, не задает наиболее общий вид стеков, но является понятием стека ограниченной емкости.

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

Рассмотрим следующую ситуацию:

-- Предупреждение: это неправильный класс, только в целях иллюстрации.

class SNEAKY feature

tricky is

require

accredited

do

...

end

feature {NONE}

accredited: BOOLEAN is do ... end

end

Спецификация для tricky устанавливает, что любой вызов этой процедуры должен удовлетворять условию, выраженному булевой функцией accredited. Но при экспорте класса эта функция для клиентов является закрытой, поэтому у них нет способа проверить выполнимость условия перед вызовом tricky. Очевидно, подобная ситуация неприемлема.

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

Это правило учитывает все возможные ситуации экспорта, а не только случаи доступности всем клиентам (tricky) или полной недоступности (accredited). Как отмечалось, при обсуждении проблемы скрытия информации, компонент класса можно сделать доступным для некоторых клиентов, явно перечислив их в feature предложении, например feature {A, B, ... }, определяющего доступность только для классов A, B, ... и их потомков. Сформулируем правило языка:

Правило Доступности предусловия

Каждый компонент, появляющийся в предусловии программы, должен быть доступен каждому клиенту, которому доступна сама программа.

В соответствии с этим правилом каждый клиент, способный вызвать программу, способен проверить ее предусловие. По этому правилу класс SNEAKY является коварным, некорректно построенным, поскольку экспортирует tricky с недоступным предусловием. Нетрудно превратить этот класс в правильно построенный, изменив статус экспорта у accredited. Если tricky появится с предложением feature в форме feature {A, B, C}, то accredited должна экспортироваться, по меньшей мере, клиентам A, B, C, появляясь в той же группе feature, что и tricky. Можно задать для accredited собственное feature-предложение в одной из форм: feature {A, B, C}, feature {A, B, C, D, ...} или просто feature. Любое нарушение этого правила приведет к ошибке в период компиляции. Класс SNEAKY, например, будет забракован компилятором.

Подобного правила нет для постусловий. Не является ошибкой в постусловии ссылаться на компоненты, закрытые или экспортируемые избранным клиентам. Просто это означает, что описание эффекта выполнения программы содержит некоторые свойства, непосредственно не используемые клиентом. Подобная ситуация имеет место в процедуре put класса STACK2:

put (x: G) is

-- Добавить элемент x на вершину

require

not full

do

...

ensure

... Другие предложения...

in_top_array_entry: representation @ count = x

end

Последнее предложение в постусловии устанавливает, что элемент массива с индексом count содержит последний втолкнутый в стек элемент. Это свойство реализации, хотя put обычно доступно (экспортируется всем клиентам), массив representation является закрытым. Но ничего ошибочного в постусловии нет. Оно просто включает наряду со свойствами, полезными для клиентов ("Другие предложения"), свойство, имеющее смысл только для тех, кто знаком с полным текстом класса. Такие закрытые предложения не будут появляться в краткой форме класса - документации, предназначенной для авторов клиентских модулей.

(При первом чтении этот раздел можно опустить или ограничиться его беглым просмотром.)

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

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

Поскольку классу понадобятся целочисленные коды ошибок, удобно для этой цели использовать ранее не введенную нотацию "unique" для целочисленных констант. Если объявить множество атрибутов следующим образом:

a, b, c, ...: INTEGER is unique

то в результате этого объявления a, b, c получат последовательно идущие целочисленные значения. Эти значения будут даваться компилятором с гарантией того, что все объявленные таким образом константы получат различные значения (будут уникальными). По принятому соглашению, всем объявляемым таким образом константам даются имена, начинающиеся с буквы в верхнем регистре и с остальными символами в нижнем регистре, например Underflow.

Вот написанная в этом стиле толерантная версия нашего класса стек. Заметьте, что этот текст, возможно пропущенный при первом чтении, включен только для понимания толерантного стиля. Он не является примером рекомендуемого стиля проектирования по причинам, обсуждаемым ниже, но которые достаточно ясны при просмотре этого текста.

indexing

description: "Стеки: Структуры с политикой доступа Last-In, First-Out %

%Первый пришел - Последний ушел, с фиксированной емкостью; %

%толерантная версия, устанавливающая код ошибки в случае %

%недопустимых операций."

class STACK3 [G] creation

make

feature - Initialization (Инициализация)

make (n: INTEGER) is

-- Создать стек, содержащий максимум n элементов, если n > 0;

-- в противном случае установить код ошибки равным Negative_size.

-- Без всяких предусловий!

do

if capacity >= 0 then

capacity := n

create representation.make (capacity)

else

error := Negative_size

end

ensure

error_code_if_impossible: (n < 0) = (error = Negative_size)

no_error_if_possible: (n >= 0) = (error = 0)

capacity_set_if_no_error: (error = 0) implies (capacity = n)

allocated_if_no_error: (error = 0) implies (representation /= Void)

end

feature - Access (Доступ)

item: G is

-- Элемент вершины, если существует; в противном случае

-- значение типа по умолчанию.

-- с ошибкой категории Underflow.

-- Без всяких предусловий!

do

if not empty then

check representation /= Void end

Result := representation.item

error := 0

else

error := Underflow

-- В этом случае результатом является значение по умолчанию

end

ensure

error_code_if_impossible: (old empty) = (error = Underflow)

no_error_if_possible: (not (old empty)) = (error = 0)

end

feature -- Status report (Отчет о статусе)

empty: BOOLEAN is

-- Пуст ли стек?

do

Result := (capacity = 0) or else representation.empty

end

error: INTEGER

-- Индикатор ошибки, устанавливаемый различными компонентами

-- в ненулевое значение, если они не могут выполнить свою работу

full: BOOLEAN is

-- Заполнен ли стек?

do

Result := (capacity = 0) or else representation.full

end

Overflow, Underflow, Negative_size: INTEGER is unique

-- Возможные коды ошибок

feature -- Element change (Изменение элементов)

put (x: G) is

-- Добавить x на вершину, если возможно; иначе задать код ошибки.

-- Без всяких предусловий!

do

if full then

error := Overflow

else

check representation /= Void end

representation.put (x); error := 0

end

ensure

error_code_if_impossible: (old full) = (error = Overflow)

no_error_if_possible: (not old full) = (error = 0)

not_empty_if_no_error: (error = 0) implies not empty

added_to_top_if_no_error: (error = 0) implies item = x

one_more_item_if_no_error: (error = 0) implies count = old count + 1

end

remove is

-- Удалить вершину, если возможно; иначе задать код ошибки.

-- Без всяких предусловий!

do

if empty then

error := Underflow

else

check representation /= Void end

representation.remove

error := 0

end

ensure

error_code_if_impossible: (old empty) = (error = Underflow)

no_error_if_possible: (not old empty) = (error = 0)

not_full_if_no_error: (error = 0) implies not full

one_fewer_item_if_no_error: (error = 0) implies count = old count - 1

end

feature {NONE} - Implementation (Реализация)

representation: STACK2 [G]

-- Незащищенный стек используется для реализации

capacity: INTEGER

-- Максимальное число элементов стека

end - class STACK3

Операции этого класса не имеют предусловий (более точно, имеют True в качестве предусловия). Результат выполнения может характеризовать ненормальную ситуацию, постусловие переопределено так, чтобы позволить отличать корректную и ошибочную обработку. Например, при вызове s.remove, где s это экземпляр класса STACK3, в корректной ситуации значение s.error будет равно 0; в ошибочной - Underflow. В последнем случае никакая другая работа выполняться не будет. Клиент несет ответственность за проверку s.error после вызова. Как уже отмечалось, у общецелевого модуля, такого как STACK3 нет способа решить, что делать в ошибочной ситуации: выдать сообщение об ошибке, произвести корректировку ситуации...

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

Несколько технических замечаний к приведенному примеру класса.

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

[x]. Булева операция or else подобна or, но если первый операнд равен True, игнорирует второй операнд, возможно неопределенный в такой ситуации.

[x]. Инструкция check, используемая в put и remove, служит для проверки выполнения некоторых утверждений. Она будет изучаться позднее в этой лекции.

В заключение: вы, наверное, отметили тяжеловесность STACK3 в сравнении с простотой STACK2, достигнутой благодаря предусловиям. Это хороший пример, показывающий, что толерантный стиль может приводить к бесполезно усложненному ПО. Требовательный стиль, по контрасту, вытекает из общего духа Проектирования по контракту. Попытка управлять всем, - и возможными и невозможными случаями - совсем не лучший способ помочь вашим клиентам. Если вместо этого вы построите классы, влекущие возможно более строгие условия на их использование, точно опишите эти условия, включив их в документацию класса, вы реально облегчите жизнь вашим клиентам. Требовательная любовь (tough love) может быть лучше всепрощающей; лучше эффективная поддержка функциональности с проверяемыми ограничениями, чем страстная попытка предугадать желания клиентов, принятие возможно неадекватных решений, жертвой чего становятся простота и эффективность.

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

Предусловия и постусловия описывают свойства отдельных программ. Но экземпляры класса обладают также глобальными свойствами. Их принято называть инвариантами класса (class invariants), и они определяют более глубокие семантические свойства и ограничения целостности, характеризующие класс.

Рассмотрим снова реализацию стека классом STACK2:

class STACK2 [G] creation

make

feature

? make, empty, full, item, put, remove?

capacity: INTEGER

count: INTEGER

feature {NONE} -- Implementation

representation: ARRAY [G]

end

Атрибуты класса - массив representation и целые capacity, count - задают представление стека. Хотя предусловия и постусловия программ отражают семантику стека, их недостаточно для выражения важных свойств, связывающих атрибуты. Например, count всегда должно удовлетворять условию:

0 <= count; count <= capacity

из которого следует, что capacity >=0 и что capacity задает размер массива:

capacity = representation.capacity

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

Выше приведенные примеры инвариантов включали только атрибуты. Инварианты могут выражать отношения между функциями и между функциями и атрибутами. Например, инвариант STACK2 может включать следующее свойство, описывающее связь между функцией empty и count:

empty = (count = 0)

Этот пример не показателен, он повторяет утверждение, заданное постусловием empty. Более полезные утверждения те, которые включают только атрибуты или более чем одну функцию.

Вот еще один типичный пример. Предположим, что мы имеем дело с банковскими счетами, и есть класс Bank_Account с компонентами: deposits_list, withdrawals_list и balance. Тогда инвариантом такого класса может быть утверждение в форме:

consistent_balance: deposits_list.total - withdrawals_list.total = balance

где функция total дает суммарное значение списка всех операций (приходных или расходных). Инвариант определяет основное условие согласования всех банковских операций над счетом, связывая баланс, приходные и расходные операции.

Синтаксически инвариант класса является утверждением, появляющимся в предложении invariant, стоящим после всех предложений feature, и перед предложением end. Вот пример:

class STACK4 [G] creation

...Как в STACK2...

feature

...Как в STACK2...

invariant

count_non_negative: 0 <= count

count_bounded: count <= capacity

consistent_with_array_size: capacity = representation.capacity

empty_if_no_elements: empty = (count = 0)

item_at_top: (count > 0) implies (representation.item (count) = item)

end

Инвариант класса C это множество утверждений, которым удовлетворяет каждый экземпляр класса во все "стабильные" времена. В эти времена экземпляр класса находится в наблюдаемом состоянии:

[x]. на момент создания экземпляра, сразу после выполнения create a или create a.make(...), где a класса C;

[x]. перед и после каждого удаленного вызова a.r(...) программы r класса С.

Следующий рисунок, показывающий жизнь объектов, поможет разобраться в инвариантах и стабильных временах:

Рис. 11.4.  Жизнь объектов

Жизнь объектов не столь уж захватывающая. Вначале - слева на рисунке - он просто не существует. При выполнении инструкции create a или create a.make(...) или clone объект создается и достигает первой станции S1 в своей жизни. Затем идет череда довольно скучных событий: клиенты, для которых доступен объект, один за другим вызывают его компоненты в форме a.f(..). Так все продолжается, пока не завершится вычисление.

Инвариант является характеристическим свойством состояний, представленных большими квадратиками на рисунке: S1, S2, S3 и т.д. Эти состояния соответствуют стабильным временам, упомянутым выше.

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

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

Закончим обсуждение правилом, точно определяющим, когда утверждение является корректным инвариантом класса:

Правило инварианта

Утверждение Inv является корректным инвариантом класса, если и только если оно удовлетворяет следующим двум условиям:

1 Каждая процедура создания, применимая к аргументам, удовлетворяющим ее предусловию в состоянии, в котором атрибуты имеют значения, установленные по умолчанию, вырабатывает заключительное состояние, гарантирующее выполнение Inv.

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

Заметьте, в этом правиле:

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

[x]. Состояние объекта определяется значениями всех его полей (значениями атрибутов класса для этого конкретного экземпляра).

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

[x]. Постусловие может включать только заключительное состояние, начальное состояние, (используя нотацию old) и, в случае функций, возвращаемое значение, заданное предопределенной сущностью Result.

[x]. Инвариант может включать только состояние.

Математическое выражение правила Инварианта появится позже в этой лекции.

Можно использовать правило Инварианта как основу для ответа на вопрос, что означает нарушение инварианта в период выполнения системы? Мы уже установили, что нарушение предусловия означает ошибку (жучок) клиента, нарушение постусловия - ошибка поставщика. Для инвариантов ответ такой же, как и для постусловий^11.2).

Свойство (2) правила инвариантов показывает, что неявно их можно рассматривать как добавления к предусловиям и постусловиям каждой экспортируемой программы класса. Посему принципиально понятие инварианта класса избыточно - это часть предусловий и постусловий программ.

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

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

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

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

Давайте пойдем дальше. Выше отмечалось, что инварианты можно рассматривать как добавки к предусловиям и постусловиям экспортируемых программ. Пусть body тело программы, pre - предусловие, post - постусловие, Inv - инвариант программы. Требование корректности программы может быть записано в виде:

{INV and pre} body {INV and post}

Это означает, что любое выполнение body, начинающееся в состоянии, удовлетворяющем Inv и pre, завершится в состоянии, в котором выполняются Inv и post. Для человека, создающего body, появление инварианта является "хорошей" или "плохой" новостью, облегчается или затрудняется его задача? Ответ, как следует из предыдущих обсуждений, и да и нет! Вспомним ленивого работника, который мечтает о сильном предусловии и слабом постусловии, чтобы можно было бы работать как можно меньше. Инвариант усиливает как предусловие, так и постусловие. Так что, если вы ответственны за реализацию body, то добавление инварианта:

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

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

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

Класс BANK_ACCOUNT, упоминавшийся выше, с инвариантом класса:

deposits_list.total - withdrawals_list.total = balance

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

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

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

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

Нотация {P} A {Q} поможет выразить наше определение более строго.

Пусть C обозначает класс, Inv - инвариант, r - программа класса. Для каждой программы Body_r - ее тело, pre_r(x_r), post_r(x_r) - ее предусловие и постусловие с возможными аргументами x_r. Если предусловие или постусловие для программы r опущены, то будем считать их заданными константой True.

Наконец, пусть Default_C обозначает утверждение, выражающее тот факт, что атрибуты класса C имеют значения по умолчанию, определенные их типами. Например, Default_STACK2 для класса STACK2 является следующим утверждением:

representation = Void

capacity = 0

count = 0

Эта нотация позволяет дать общее определение корректности класса:

Определение: Корректность класса

Класс C корректен по отношению к своим утверждениям, если и только если:

1

Для любого правильного множества аргументов x_p процедуры создания p:

{Default_C and pre_p(x_p)} Body_p {post_p(x_p) and Inv}

2

Для каждой экспортируемой программы r и для любого множества правильных аргументов x_r:

{pre_r(x_r) and Inv} Body_r {post_r(x_r) and Inv}

Это правило является математической формулировкой ранее рассмотренной неформальной диаграммы, показывающей жизненный цикл типичного объекта (рис. 11.4). Условие (1) означает, что любая процедура создания при ее вызове с выполняемым предусловием должна вырабатывать начальное состояние (S1 на рисунке), удовлетворяющее постусловию и инварианту. Условие (2) отражает тот факт, что любая экспортируемая процедура r (f и g на рисунке), вызываемая в состояниях (S1, S2, S3), удовлетворяющих предусловию и инварианту, должна завершаться в состояниях, удовлетворяющих постусловию и инварианту.

Два практических замечания:

[x]. Если у класса нет предложения creation, то можно полагать, что существует неявная процедура создания по умолчанию - nothing с пустым телом. Применение правила (1) к B_nothing в этом случае означает, что Default_C влечет Inv; другими словами, значения полей по умолчанию должны удовлетворять инварианту в этом случае.

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

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

Инвариант класса задает множество свойств объектов (экземпляров класса), которые должны выполняться в стабильные времена жизни объектов. В частности, эти свойства должны выполняться сразу после создания экземпляра объекта.

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

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

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

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

indexing

description: "Последовательности значений одного типа или %

%согласованных типов, доступных по индексам - целым из заданного интервала %"

class ARRAY [G] creation

make

feature - Initialization (Инициализация)

make (minindex, maxindex: INTEGER) is

-- Создать массив с границами minindex и maxindex

-- (пустой если minindex > maxindex).

require

meaningful_bounds: maxindex >= minindex - 1

do

...

ensure

exact_bounds_if_non_empty: (maxindex >= minindex) implies

((lower = minindex) and (upper = maxindex))

conventions_if_empty: (maxindex < minindex) implies

((lower = 1) and (upper = 0))

end

feature -- Access (Доступ)

lower, upper, count: INTEGER

-- Минимальное и максимальное значение индекса; размер массива.

infix "@", item (i: INTEGER): G is

-- Элемент с индексом i

require

index_not_too_small: lower <= i

index_not_too_large: i <= upper

do ... end

feature -- Element change (Изменение элементов)

put (v: G; i: INTEGER) is

-- Присвоить v элементу с индексом i

require

index_not_too_small: lower <= i

index_not_too_large: i <= upper

do

...

ensure

element_replaced: item (i) = v

end

invariant

consistent_count: count = upper - lower + 1

non_negative_count: count >= 0

end

Единственное, что не конкретизировано в описании этого класса, это реализация программ item и put. Поскольку эффективная манипуляция с массивом требует доступа к системам низкого уровня, то эти программы будут реализованы с использованием внешних классов, что будет рассмотрено в последующих лекциях.

Класс, как неоднократно говорилось, является реализацией АТД, заданного формальной спецификацией или неявно подразумеваемого. В начале лекции отмечалось, что утверждения можно рассматривать, как способ введения в класс семантических свойств, лежащих в основе АТД. Давайте уточним наше понимание концепции утверждений, прояснив их связь с компонентами спецификации АТД.

Как отмечалось в лекции про АТД, они включают четыре элемента:

[x]. имя типа, возможно с родовым параметром (раздел TYPES);

[x]. список функций с их сигнатурами (раздел FUNCTIONS);

[x]. аксиомы, выражающие свойства результатов функций (раздел AXIOMS);

[x]. ограничения применимости функций (раздел PRECONDITIONS).

При поверхностном применении АТД часто опускают две последние части. Во многом, это лишает данный подход привлекательности, поскольку предусловия и аксиомы выражают семантические свойства функций. Если их опустить и просто рассматривать стек как инкапсуляцию операций put, remove и других, то преимущества от скрытия информации останутся, но это все. Понятие стека становится пустой оболочкой без семантики, кроме той, что остается в именах функций. (В этой книге имена функций менее информативны по причине согласованности и повторного использования, - мы сознательно выбрали общие имена - put, remove, item, а не те, которые применяются обычно для стеков - push, pop, top).

Этот риск потери семантики переносится на программирование: программы, реализующие операции соответствующего АТД, в принципе могут выполнять нечто отличное от задуманного. Утверждения предотвращают этот риск, возвращая семантику классу.

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

f : A × B × ... X

зависит от того, где имя АТД, скажем T, встречается среди типов A, B, ... X, включенных в эту сигнатуру:

[x]. Если Т появляется только справа от стрелки, f является создателем; в классе это соответствует процедуре создания.

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

[x]. Если Т появляется как слева, так и справа от стрелки, f является командой, вырабатывающей новый объект из одного или нескольких уже существующих. На этапе реализации f часто задается процедурой (также называемой командой), которая модифицирует существующий объект, не создавая новый, как это делают функции.

Из соответствия между АТД функциями и компонентами класса можно вывести соответствие между утверждениями класса и семантическими свойствами АТД.

[x]. Предусловие для специфицированной в АТД функции появляется как предусловие программы, соответствующей данной функции.

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

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

[x]. Аксиомы, включающие функцию создатель, появятся в постусловии соответствующей процедуры создания.

В этот момент следует вернуться назад и сравнить аксиомы АТД STACK с утверждениями класса STACK4 (включая и те, которые даны для класса STACK2).

Этот раздел требует от читателя определенной математической подготовки.

Полезно рассмотреть предшествующее обсуждение в терминах следующего рисунка, навеянного работой [Hoare 1972a], в которой описывается понятие "С является корректной реализацией А".

Рис. 11.5.  Преобразования между абстрактными и конкретными объектами

Здесь А - АТД, С - класс, его реализующий. Абстрактной функции af из спецификации АТД соответствует в классе конкретная функция cf. Для простоты, полагаем, что абстрактная функция af из A возвращает результат того же типа А.

Стрелка, помеченная а, представляет функцию абстракции (abstraction function), которая для любого экземпляра класса - конкретного объекта - возвращает соответствующий абстрактный объект (экземпляр АТД). Как будет видно, функция обычно бывает частичной, а обратное отношение обычно не является функцией.

Реализация корректна, если (для всех функций af из АТД и их реализаций cf) диаграмма коммутативна, или, как говорят, имеет место:

Свойство согласованности Класс-АТД

(cf;a) = (a;af)

где символ ";" обозначает композицию функций. Другими словами, для любых двух функций f и g, их композиция: f;g задает функцию h, такую что h(x) = g(f(x)) для каждого применимого x.

(Композицию f;g также записывают в виде: g ° f, с обратным порядком применения операндов.)

Свойство устанавливает, что для каждого конкретного объекта CONC_1 не имеет значения, в каком порядке применяются преобразования (функция абстракции, а затем af или вначале cf, а потом функция абстракции); оба пути, помеченные на рисунке штрихованными линиями, ведут к одному и тому же значению - абстрактному объекту ABST_2. Результат будет одним и тем же, если:

[x]. Применить конкретную функцию класса cf, а потом функцию абстракции а, получив a(cf(CONC_1)).

[x]. Применить функцию абстракции а, а потом функцию АТД - af, получив af(a(CONC_1)).

Некоторые утверждения появляются в реализации, хотя они не имеют прямых двойников в спецификации АТД. Эти утверждения используют атрибуты, включая некоторые закрытые атрибуты, которые, по определению, не имеют смысла в АТД. Простым примером являются свойства, появляющиеся в инварианте STACK4:

count_non_negative: 0 <= count

count_bounded: count <= capacity

Такие утверждения составляют часть инварианта класса, известную как инвариант реализации (implementation invariant). Они позволяют задать соответствие представления реализации, выбранное в классе, (здесь это атрибуты count, capacity, representation) - визави соответствующего АТД.

Рис. 11.5 помогает понять концепцию инварианта реализации. Он иллюстрирует характеристические свойства функции абстракции, представленной вертикальной стрелкой на рисунке. Об этом стоит поговорить подробнее.

Прежде всего, корректно ли рассматривать а, как функцию? Напомним, что функция (тотальная или частичная) отображает каждый элемент исходного множества ровно в один элемент целевого множества, в противоположность общему случаю отношения, не имеющего такого ограничения. Рассмотрим обратное преобразование (сверху - вниз) от абстрактного объекта к конкретному. Будем называть его отношением представления (representation relation); как правило, это отношение не является функцией, так как существует множество представлений одного и того же абстрактного объекта. В реализации стека массивом, где каждый стек задан парой <representation, count>, абстрактный стек имеет много различных представлений, иллюстрируемых следующим рис. 11.6. Все они имеют одно и то же значение count и одинаковые элементы массива representation для всех индексов в пределах от 1 до count, но размер массивов - capacity - может быть любым значением, большим или равным count; элементы массива с индексом, большим count могут содержать произвольные значения.

Так как интерфейс класса ограничен компонентами, непосредственно выводимыми из функций АТД, клиенты не имеют способа различать поведение конкретных объектов, представляющих один и тот же абстрактный стек (это и есть причина, по которой все они имеют одну функцию абстракции a). Заметьте, в частности, что процедура remove из STACK4 выполняет свою работу, просто изменяя count

count := count - 1

не пытаясь очистить выше расположенные элементы. Всякое изменение элементов, расположенных выше count, будет модифицировать конкретный стек CS, не оказывая никакого влияния на ассоциированный абстрактный стек a(CS).

Итак, отношение реализации это обычно не функция. Но инверсия этого отношения - функция абстракции - действительно является функцией, так как каждому конкретному объекту ставится в соответствие один абстрактный объект. В примере стека каждой правильной паре <representation, count> соответствует в точности один абстрактный стек. У него count элементов, растет снизу вверх, элементы representation имеют индексы в пределах от 1 до count.

Рис. 11.6.  Один абстрактный объект и два его представления

Оба конкретных стека, изображенные на рисунке, являются реализациями абстрактного стека, состоящего из трех элементов со значениями: 342, -133, 5. Отображение а должно быть функцией, иначе конкретный объект мог быть интерпретирован как реализация двух или более различных абстракций. В этом случае выбранная реализация двусмысленна и, следовательно, неадекватна. Поэтому стрелка, ассоциированная с а, правильно отображает существующую функциональную зависимость между абстрактными и конкретными типами. (Обсуждение наследования будет делаться при тех же предположениях).

Функция абстракции а обычно представима частичной функцией: не для каждого возможного конкретного объекта существует правильное представление абстрактного объекта. Например, не каждая пара <representation, count> является правильным представлением абстрактного стека. Если representation является массивом емкости 3 и count = 4, то они совместно не представляют абстрактный стек. Правильные представления (члены, входящие в область определения функции абстракции), - только те пары, для которых count находится между 0 и размерностью массива. Это свойство является инвариантом реализации.

В математических терминах, инвариант реализации является характеристической функцией области определения абстрактной функции. Другими словами, это булево свойство, определяющее применимость функции. (Характеристическая функция подмножества А задает булево свойство, истинное на А и ложное всюду вне его.)

Инвариант реализации является той частью утверждений класса, у которой нет двойника в спецификации АТД. Он не связан с АТД, и относится только к реализации. Он определяет, при каких условиях кандидат - конкретный объект - действительно является реализацией одного и только одного абстрактного объекта.

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

Можно рассматривать и другие возможности использования утверждений. Хотя они менее специфичны для нашего метода, но тоже играют важную роль, и должны быть частью нашей нотации. Наши расширения будут включать инструкцию проверки check, а также конструкции, задающие корректность цикла (инварианты и варианты цикла), рассматриваемые в следующем разделе.

Инструкция check выражает уверенность автора программы, что некоторое свойство всегда выполняется, когда вычисление достигает точки, в которой находится наша инструкция. Синтаксически, инструкция записывается в следующей форме:

check

assertion_clause1

assertion_clause2

...

assertion_clausen

end

Включив эту инструкцию в программный текст, мы говорим, что всякий раз, когда управление достигает этой инструкции, заданное утверждение (предложения утверждения между check и end) должно выполняться.

Это некоторый способ убеждать самого себя, что некоторые свойства выполняются. Более важно, что это позволяет будущим читателям вашего программного текста понять, на каких гипотезах вы основываетесь. Создание ПО требует многочисленных предположений о свойствах объектов системы. Тривиальный, но типичный пример - вызов sqrt(x) предполагает x>=0. Это предположение может быть очевидным из контекста, например, если вызов является частью условного оператора в форме:

if x >= 0 then y := sqrt (x) end

Но проверка может быть чуть менее очевидной, если, например:

x := a^2 + b^2

Инструкция check дает возможность выразить наше предположение о свойствах объектов:

x := a^2 + b^2

... Другие инструкции ...

check

x >= 0

-- Поскольку x был вычислен как сумма квадратов.

end

y := sqrt (x)

Здесь нет конструкции if... then..., защищающей вызов sqrt; но check показывает, что вызов корректен. Хорошей практикой является сопровождать инструкцию комментарием с обоснованием утверждения, как это сделано в примере. Отступы при записи инструкции это тоже часть рекомендованного стиля; они подчеркивают, что при нормальных обстоятельствах инструкция проверки никак не влияет на ход алгоритмического процесса вычислений.

Этот пример типичен для демонстрации того, что наиболее вероятное применение инструкции проверки состоит в добавлении ее, как раз перед вызовом программы, имеющей предусловие. В качестве еще одного примера рассмотрим вызов

s.remove

в точке, где вы точно знаете, что стек s не пуст, поскольку до этого в стек засылалось n элементов, а удалялось m, и вам известно, что n>m. В этом случае нет необходимости защищать вызов: if (not s.empty) then ...; но, если причина корректности вызова непосредственно следует из контекста, то есть смысл напомнить читателю, что "беззащитный" вызов является осознанным решением, а не недосмотром. Этого можно достичь, добавляя проверку:

check not s.empty end

Вариант такой ситуации встречается, когда пишется вызов в форме x.f в полной уверенности, что x/=Void, так что нет необходимости заключать этот вызов в оператор if (x/=Void) then ..., но, тем не менее, существование x не очевидно из контекста. Вернемся к рассмотрению процедур put и remove нашего "защищенного" класса STACK3. Вот текст тела процедуры put:

if full then

error := Overflow

else

check representation /= Void end

representation.put (x); error := 0

end

Здесь читатель может думать, что вызов в else ветви: representation.put(x) потенциально не безопасен, поскольку ему не предшествует тест: (representation /=Void). Но, исследуя текст класса, можно понять, что из условия (full = false) следует положительность capacity, откуда, в свою очередь, следует, что representation не может быть Void. Это важное и не совсем тривиальное свойство, которое должно быть частью инварианта реализации класса. Фактически, с полностью установленным инвариантом реализации следует переписать инструкцию проверки следующим образом:

check

representation_exists: representation /= Void

-- Поскольку предложение representation_exists истинно, когда

-- full ложно, что следует из инварианта реализации.

end

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

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

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

Но с мощностью приходят и риски. У циклов дурная слава, - их трудно заставить работать правильно. Типичными для циклов являются:

[x]. Ошибки "больше-меньше" (выполнение цикла слишком много или слишком мало раз).

[x]. Ошибки управления пограничными ситуациями, например пустыми структурами. Цикл может правильно работать на больших массивах, но давать ошибки, когда у массива один элемент или он вообще пуст.

[x]. Ошибки завершения ("зацикливание") в некоторых ситуациях.

Бинарный поиск - один из ключевых элементов базового курса "Введение в информатику" (Computer Science 101) - хорошая иллюстрация "коварства" циклов даже в относительно тривиальной ситуации. Рассмотрим целочисленный, упорядоченный по возрастанию массив t с индексами от 1 до n. Используем алгоритм бинарного поиска для ответа на вопрос: появляется ли целое x среди элементов массива. Если массив пуст, ответ должен быть "нет", если в массиве ровно один элемент, то ответ "да" тогда и только тогда, когда элемент массива совпадает с x. Суть бинарного поиска, использующего упорядоченность массива, проста: вначале x сравнивается со средним элементом массива, если есть совпадение, то задача решена, если x меньше среднего элемента, то поиск продолжается в верхней половине массива, в противном случае - в нижней половине. Каждое сравнение уменьшает размер массива вдвое. Ниже представлены четыре попытки реализации этой простой идеи. К несчастью, все они содержат ошибки. Вам предоставляется случай поупражняться в поиске ошибок и установить, в какой ситуации каждый из алгоритмов не работает нужным образом.

Таблица 11.3.Четыре (ошибочных) попытки реализации бинарного поиска

Разумное использование утверждений может помочь справиться с такими проблемами. Цикл может иметь связанное с ним утверждение, так называемый инвариант цикла (loop invariant), который не следует путать с инвариантом класса. Он может также иметь вариант цикла (loop variant), являющийся не утверждением, а, обычно целочисленным выражением. Совместно, инвариант и вариант позволяют гарантировать корректность цикла.

Для понимания этих понятий необходимо осознать, что цикл - это способ вычислить некоторый результат последовательными приближениями (successive approximations).

Рассмотрим тривиальный пример вычисления максимума в целочисленном массиве, используя очевидный алгоритм:

maxarray (t: ARRAY [INTEGER]): INTEGER is

-- Максимальное значение массива t

require

t.capacity >= 1

local

i: INTEGER

do

from

i := t.lower

Result := t @ lower

until i = t.upper loop

i := i + 1

Result := Result.max (t @ i)

end

end

В разделе инициализации i получает значение нижней границы массива, а сущность Result - будущий результат вычислений - значение первого элемента. Предусловие гарантирует существование хотя бы одного элемента в массиве. Производя последовательные итерации в цикле, мы достигаем верхней границы массива, увеличивая на каждом шаге i на 1, и заменяя Result значением элемента t @ i, если этот элемент больше чем Result. Для нахождения максимума двух целых используется функция max, определенная для класса integer: a.max(b) возвращает максимальное значение из a и b.

Это пример вычисления последовательными приближениями. Мы продвигаемся вверх по массиву последовательными нарезками: [lower, lower], [lower, lower+1], [lower, lower+2] и так вплоть до полного приближения [lower, upper].

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

Рис. 11.7.  Аппроксимация массива последовательными нарезками

Простой пример вычисления максимума массива иллюстрирует общую схему циклических вычислений, применимую ко многим ситуациям. Вы определяете, что решением некоторой проблемы является элемент, принадлежащий n-мерной поверхности POST. В некоторых случаях POST может содержать ровно один элемент - решение, но обычно может быть более чем одно приемлемое решение проблемы. Циклы полезны, когда нет прямого способа достичь решения "одним выстрелом". Но у вас есть непрямая стратегия, вы можете, например, прицелиться и попасть в m-мерную поверхность INV, включающую POST (для m>n). Инвариантом является то, что поверхность попадания все время содержит POST. Итерация за итерацией приближаемся к POST, сохраняя истинность INV. Следующий рисунок иллюстрирует этот процесс:

Рис. 11.8.  Вычисление цикла (из [М 1990])

Вычисление цикла имеет следующие ингредиенты:

[x]. Цель post, определяемую как свойство, выполняемое в любом допустимом заключительном состоянии. Пример: "Result является максимумом массива". На рисунке цель post представлена множеством состояний POST.

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

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

[x]. Преобразование body, начинающееся в INV, но не в POST, вырабатывающее точку более близкую к POST, но все еще остающуюся в INV. Тело цикла функции maxarray является примером подобного преобразования.

[x]. Верхняя граница числа применений body, необходимого для перевода точки из INV в POST. Как будет пояснено ниже, этот параметр необходим для определения варианта.

Последовательные приближения один из главных инструментов численного анализа. Но там эта идея понимается шире. Важная разница состоит в том, что в чистой математике допускаются бесконечные вычисления, последовательность может иметь предел, даже если он не достигается конечным числом приближений. Последовательность 1/n имеет предел 0, хотя среди членов последовательности нет числа 0. В компьютерных вычислениях мы хотим видеть результаты на нашем экране еще при нашей жизни, так что мы настаиваем, все аппроксимирующие последовательности достигают своей цели после конечного числа итераций.

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

[x]. Вариант всегда не отрицателен.

[x]. Любое выполнение тела цикла уменьшает вариант.

Так как целочисленная неотрицательная величина не может уменьшаться бесконечно, то наличие варианта позволяет гарантировать завершение цикла. Вариант является верхней границей, максимальным числом применений body, приводящим точку в POST. В задаче нахождения максимума найти вариант просто: t.upper - i. Это выражение удовлетворяет обоим условиям:

[x]. Предусловие программы требует положительности t.capacity; другими словами, программа применима только к непустым массивам. Инвариант класса ARRAY задает: capacity = upper - lower + 1. Отсюда следует, что свойство i <= t.upper будет выполняться после инициализации i значением t.lower.

[x]. Любое выполнение тела цикла выполняет инструкцию i := i + 1, уменьшая вариант на единицу.

В этом примере цикл является простым итерированием на последовательности целых чисел в конечном интервале, известный в языках программирования, как "цикл For" или "цикл DO", завершение которого не трудно проверить. Для более изощренных циклов число требуемых итераций определить не так просто, выявление завершения становится сложной задачей, единственным универсальным способом является нахождение варианта.

Нам понадобится еще одно понятие, преобразующее только что набросанную схему в программный текст, описывающий цикл. Мы нуждаемся в простом способе определения того, что текущая итерация достигла цели (постусловия) post. Поскольку итерация конструируется так, чтобы обеспечить выполнение INV, а POST является частью INV, то обычно можно найти условие exit такое, что элемент из INV принадлежит POST тогда и только тогда, когда выполняется exit. Другими словами, постусловие post и инвариант inv связаны соотношением:

post = inv and exit

так что мы можем остановить цикл, - чьи промежуточные состояния по построению удовлетворяют inv, - как только выполнится exit. В этом состоянии, следовательно, будет выполнено и post.

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

[x]. Инвариант цикла inv - утверждение.

[x]. Условие выхода exit, чья конъюнкция с inv дает желаемую цель.

[x]. Вариант var - целочисленное выражение.

[x]. Множество инструкций инициализации, которые всегда приводят к состоянию, в котором inv выполняется, а var становится неотрицательным.

[x]. Множество инструкций body, которое (при условии, что оно начинается в состоянии, где var неотрицательно и выполняется inv), сохраняет инвариант и уменьшает var, в то же время следя за тем, чтобы оно не стало меньше нуля.

[x]. Синтаксис цикла честно комбинирует эти ингредиенты:

from

init

invariant

inv

variant

var

until

exit

loop

body

end

Предложения invariant и variant являются возможными. Предложение from по синтаксису требуется, но инструкция init может быть пустой.

Эффект выполнения цикла можно описать так: вначале выполняется init, затем 0 или более раз выполняется тело цикла, которое перестает выполняться, как только exit принимает значение false.

В языках Pasal, C и других такой цикл называется "циклом while", в отличие от цикла типа "repeat ... until", в котором тело цикла выполняется, по меньшей мере, один раз. Здесь же тест является условием выхода, а не условием продолжения, и синтаксис цикла явно содержит фазу инициализации. Потому эквивалент записи нашего цикла на языке Pascal выглядит следующим образом:

init;

while not exit do body

С вариантами и инвариантами цикл для maxarray выглядит так:

from

i := t.lower; Result := t @ lower

invariant

-- Result является максимумом нарезки массива t в интервале [t.lower,i].

variant

t.lower - i

until

i = t.upper

loop

i := i + 1

Result := Result.max (t @ i)

End

Заметьте, инвариант цикла выражен неформально, в виде комментария. Последующее обсуждение в этой лекции объяснит это ограничение языка утверждений.

Вот еще один пример, ранее показанный без вариантов и инвариантов. Целью следующей функции является вычисление наибольшего общего делителя - НОД (gcd - greatest common divisor) двух положительных целых a и b, следуя алгоритму Эвклида:

gcd (a, b: INTEGER): INTEGER is

-- НОД a и b

require

a > 0; b > 0

local

x, y: INTEGER

do

from

x := a; y := b

until

x = y

loop

if x > y then x := x - y else y := y - x end

end

Result := x

ensure

-- Result является НОД a и b

end

Как узнать, что функция gcd удовлетворяет своему постусловию и действительно вычисляет наибольший общий делитель a и b? Для проверки этого следует заметить, что следующее свойство истинно после инициализации цикла и сохраняется на каждой итерации:

x > 0; y > 0

-- Пара <x, y> имеет тот же НОД, что и пара <a, b>

Это и будет служить инвариантом цикла inv. Ясно, что inv выполняется после инициализации. Если выполняется inv и условие цикла x /= y, то после выполнения тела цикла:

if x > y then x := x - y else y := y - x end

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

x = y and «Пара <x, y> имеет тот же НОД, что и пара <a, b>»

Отсюда, в свою очередь, следует, что x является наибольшим общим делителем. По определению НОД (x, x) = x.

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

from

x := a; y := b

invariant

x > 0; y > 0

-- Пара <x, y> имеет тот же НОД, что и пара <a, b>

variant

x.max (y)

until

x = y

loop

if x > y then x := x - y else y := y - x end

end

Как отмечалось, предложения invariant и variant являются возможными. Когда они присутствуют, то помогают прояснить цель цикла и проверить его корректность. Для любого нетривиального цикла характерны интересные варианты и инварианты; многие из примеров в последующих лекциях включают варианты и инварианты, обеспечивая глубокое понимание корректности лежащих в основе алгоритмов.

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

[x]. Помощь в создании корректного ПО.

[x]. Поддержка документирования.

[x]. Поддержка тестирования, отладки и гарантия качества.

[x]. Поддержка приемлемого способа обработки неисправностей.

Только два последних пункта предполагают мониторинг утверждений в период выполнения.

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

Ключевая идея этой лекции - Проектирование по контракту. Использование компонент некоторого модуля является контрактом с его службами. Хорошие контракты точно специфицируют и ограничивают права и обязанности каждого участника. В проектировании ПО, где корректность и устойчивость так важны, необходимо раскрытие терминов контракта, как предварительное условие их следованию. Утверждения дают способ точно установить, что ожидается и что гарантируется каждой стороне в этом соглашении.

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

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

Вот пример краткой формы класса STACK4:

indexing

description: "Стеки: Структуры с политикой доступа Last-In, First-Out %

%Первый пришел - Последний ушел, с фиксированной емкостью"

class interface STACK4 [G] creation

make

feature -- Initialization (Инициализация)

make (n: INTEGER) is

-- Создать стек, содержащий максимум n элементов

require

non_negative_capacity: n >= 0

ensure

capacity_set: capacity = n

end

feature -- Access (Доступ)

capacity: INTEGER

-- Максимальное число элементов стека

count: INTEGER

-- Число элементов стека

item: G is

-- Элемент в вершине стека

require

not_empty: not empty -- i.e. count > 0

end

feature -- Status report (Отчет о статусе)

empty: BOOLEAN is

-- Пуст ли стек?

ensure

empty_definition: Result = (count = 0)

end

full: BOOLEAN is

-- Заполнен ли стек?

ensure

full_definition: Result = (count = capacity)

end

feature -- Element change (Изменение элементов)

put (x: G) is

-- Втолкнуть x в вершину стека

require

not_full: not full

ensure

not_empty: not empty

added_to_top: item = x

one_more_item: count = old count + 1

end

remove is

-- Удалить элемент вершины стека

require

not_empty: not empty -- i.e. count > 0

ensure

not_full: not full

one_fewer: count = old count - 1

end

invariant

count_non_negative: 0 <= count

count_bounded: count <= capacity

empty_if_no_elements: empty = (count = 0)

end

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

Если сравнить краткую форму утверждений с их оригиналами в классе, то можно заметить, что исчезли все предложения, включающие representation, так как этот атрибут не экспортируется.

Краткая форма документации особенно интересна по следующим причинам:

[x]. Документация является более высокой формой абстракции, чем объект, который она описывает. Это основное требование, предъявляемое к качественной документации. Фактическая реализация, описывающая "как", удаляется. Утверждения, объясняющие "что", а в некоторых случаях и "почему", остаются. Сохраняются заголовочные комментарии к программам и описания, включаемые в предложение indexing, дополняющие в менее формальной форме утверждения, поясняя цель и назначение программы.

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

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

Интересно сравнить этот подход с понятием интерфейса пакета в языке Ada, где модуль (пакет) состоит из двух частей - интерфейса и реализации. Java использует подобный механизм. Интерфейс пакета имеет некоторое сходство с краткой формой, но имеет и существенные различия:

[x]. Здесь нет утверждений, так что вся спецификация сводится к объявлению типов и комментариям.

[x]. Интерфейс не создается автоматически, а пишется независимо от реализации. Поэтому разработчик дважды должен задавать многие вещи: заголовки программ, их сигнатуры, комментарии к заголовкам, объявления открытых переменных. Эта навязанная избыточность утомительна (вдвойне при включении утверждений) и, как обычно, повышает риск несоответствия; всегда есть шанс, обновить одну часть и забыть про другую.

Краткая форма, дополненная ее вариантом - плоско-краткой формой (flat-short form), изучаемой при рассмотрении наследования, является принципиальным вкладом в ОО-метод. В повседневной практике ОО-разработки она появляется не только как средство документирования, но и как стандартный формат, в котором разработчики и менеджеры изучают существующие проекты, разрабатывают новые и обсуждают предложения по изменению проектов.

Краткая форма играет центральную роль в ОО-разработке, поскольку она удовлетворяет цели, определенной при анализе требований, обеспечивающих повторное использование. Суть требования: основой повторного использования являются абстрактные модули. Класс в его краткой или плоско-краткой форме является тем самым разыскиваемым абстрактным модулем.

Пришло время, дать полный ответ на вопрос: "какой эффект производят утверждения в период выполнения?". Как отмечалось, ответ определяется разработчиком, имеющим возможность управлять параметрами компиляции. Выбор нужных параметров не требует изменения текста класса, вместо этого меняется содержимое Ace файла. Напомню, Ace файл написан на языке Lace, описывающем компиляцию и сборку системы.

Вот пример применения Ace файла, устанавливающего некоторые параметры мониторинга утверждений:

system painting root

GRAPHICS

default

assertion (require)

cluster

base_library: "\library\base"

graphical_library: "\library\graphics"

option

assertion (all): BUTTON, color_BITMAP

end

painting_application: "\user\application"

option

assertion (no)

end

end -- system painting

Предложение default указывает, что для большинства классов системы проверяться будут только предусловия (require). Два кластера переопределяют установки умолчания. Кластер graphical_library будет наблюдать за всеми (all) утверждениями в классах BUTTON и color_BITMAP. Кластер painting_application вообще отменяет наблюдение за утверждениями во всех его классах. Этот пример иллюстрирует возможности мониторинга на разных уровнях - всей системы, отдельных кластеров, отдельных классов.

Следующие ключевые слова, управляющие проверкой утверждений, могут появиться в круглых скобках assertion(...):

[x]. no - не выполнять никакое из утверждений. В этом режиме оказывают на выполнение не больший эффект, чем комментарии;

[x]. require - только проверка выполнимости предусловий на входе программ;

[x]. ensure - проверка выполнимости постусловий на выходе из программы;

[x]. invariant - проверка выполнимости инвариантов класса на входе и выходе программы для квалифицированных вызовов (obj.f);

[x]. loop - проверка выполнимости инвариантов цикла перед и после каждой итерации; проверка уменьшения вариантов на каждой итерации с сохранением их не отрицательности;

[x]. check - выполнение предложений check, проверяющих выполнимость соответствующих утверждений. Ключевое слово all является синонимом check.

За исключением "no" каждый уровень автоматически влечет выполнение всех предыдущих уровней. В частности, не имеет смысла управлять постусловиями, если не проверить выполнимость предусловий. Этим объясняется эквивалентность check и all.

При включенном мониторинге пока утверждения выполняются никакого видимого эффекта на процесс вычислений они не оказывают, если не считать затрат процессорного времени. Но если одно из утверждений принимает значение false, то это довольно серьезное событие, приводящее обычно к завершению работы. Фактически, возбуждается исключение, и, если не принять специальных мер по захвату этого исключения, то выполнение остановится. При этом, однако, будет создана таблица истории исключения (exception history table) в ее общей форме:

Failure: object: O2 class: YOUR_CLASS routine: your_routine

Cause: precondition violation, clause: not_too_small

Called by: object: O2 class: YOUR_CLASS routine: his_routine

Called by: object: O1 class: HER_CLASS routine: her_routine

...

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

Возможные метки, допускаемые в утверждениях, такие как not_too_small в

your_routine (x: INTEGER) is

require

not_too_small: x >= Minimum_value

...

перечисляются при трассировке исключения, что помогает идентифицировать, что же именно пошло не так.

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

В экстремальных ситуациях все ясно:

[x]. При тестировании системы или очередной ее версии следует включать на самом высоком уровне мониторинг классов (для используемых библиотек это не обязательно). Эта возможность - один из принципиальных вкладов метода, представленного в этой книге. Мало кто из людей осознавал мощь этих идей, и как основательно они влияют на практику разработки ПО. Перелом наступил, когда фактически был получен опыт тестирования больших систем с утверждениями, включающих механизм мониторинга, описанный в этом разделе.

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

Последний совет парадоксален, при отсутствии формальных доказательств корректности говорить о "полной степени доверия" вряд ли возможно. Стоит привести красноречивое высказывание C. A. Hoare:

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

Проверка предусловий - это параметр, устанавливаемый по умолчанию в Ace файле. Его появление в примере не было необходимым.

Этот параметр особенно интересен для библиотек. Вспомните, о чем говорит основное правило нарушения утверждений. За ошибку выполнения предусловия отвечает клиент. Если вы используете повторно используемые библиотеки, предположительно высокого качества, то обычно мониторинг их постусловий и инвариантов нежелателен, хотя ошибки в библиотеках, конечно, возможны, но априорно ошибки в клиентском ПО более вероятны. Но даже для совершенных во всех отношениях библиотек следует включать проверку предусловий с единственной целью - найти ошибки клиентов.

Вероятно, наиболее очевидным примером является проверка границ массива. В классе ARRAY мы видели, что put, item и его синоним - инфиксный знак операции @, - все они имеют предусловие:

index_not_too_small: lower <= i

index_not_too_large: i <= upper

Включение предусловий для класса решает хорошо известную проблему любого продукта, использующего массивы: возможность выхода индекса за границы массива, что приводит к попаданию в область памяти, отведенную другим данным или коду, и может иметь разрушительные последствия. Большинство компиляторов предлагают специальный параметр компиляции, позволяющий управлять доступом к массиву в период выполнения. Но в объектной технологии массивы рассматриваются с общих позиций класса и объектов, а не как специальные конструкции. Мониторинг границ становится доступным благодаря общему механизму проверки условий. Просто скомпилируйте класс ARRAY, включив assertion(require).

Следует ли всегда включать проверку границ? Вот что говорит по этому поводу Тони Хоар:

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

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

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

Но, между прочим, каковы они? Ясно, что многое зависит от того, что делает ПО, и как много в нем утверждений, но можно сообщить некоторые эмпирические наблюдения. По опыту ISE стоимость мониторинга предусловий (параметр по умолчанию, включающий, конечно, и проверку границ массивов) составляет 50%. Что самое удивительное, - 75% этой стоимости не связано с проверкой предусловий, а идет на поддержку трассировки вызовов, чтобы при нарушении предусловия можно было точно сказать, кто нарушил и где. Это может быть названо Парадоксом Проверки Предусловия: проверка предусловия сама по себе недорого стоит, но, чтобы получить ее, нужно заплатить за дополнительные услуги. Что касается постусловий и инвариантов, то штраф может достигать от 100% до 200%.

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

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

В действительности, эффективность - часть корректности. Рассмотрим метеорологическую систему, требующей 12 часов работы для выработки прогноза на следующие сутки. Система тщательно оптимизирована, в частности исключены все проверки, в том числе выход индекса за границы и другие подобные неисправности. Она тщательно разрабатывалась и тестировалась. Теперь, предположим, что добавление проверок периода исполнения вдвое увеличит время ее работы. Будет ли включена проверка, - нет!

Давайте не остановимся на этом, а зададим действительно трудный вопрос. Предположим, что 12 часов уходит на работу системы с включенными проверками, Хотелось ли бы вам удалить их, чтобы получить прогноз за 6 часов, а не за 12, или тратить те же 12 часов, но перейти к более сложному алгоритму, дающему лучший прогноз? Я думаю, что если предлагается "возможность выключить проверки в интересах эффективности производственной системы", почти каждый ответит "да".

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

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

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

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

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

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

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

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

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

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

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

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

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

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

index_not_too_small: 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]

формально может быть выражен так

Result = (t.slice (lower, i)).max

в предположении, что slice вырабатывает нарезку - массив с индексами от lower до i, - а функция max дает максимальный элемент этого массива.

Ясно, чем мы рискуем: появление функций в выражениях означает введение потенциально императивных элементов (программ) в чисто аппликативный, до сего времени, мир утверждений. Без функций мы имели ясное и четкое разделение ролей, обсуждаемое ранее: инструкции предписывают, утверждения описывают. Теперь мы открыли ворота аппликативного города императивным полчищам.

Все же трудно сопротивляться мощи использования функций, поскольку все альтернативы имеют свои недостатки.

[x]. Включение полного языка спецификаций, как отмечалось, приводит к потере эффективности и простоты изучения.

[x]. Вероятно, хуже то, что неясно, достаточны ли общепринятые языки утверждений. Возьмем, например, такого естественного кандидата, в которого многие верят, - язык логики предикатов первого порядка. Этот формализм не позволяет нам выразить некоторые свойства, представляющие непосредственный интерес для разработчиков и часто используемые в утверждениях, такие как, например, "граф не имеет циклов" (типичный инвариант цикла). Математически это может быть выражено как r⁺ r = , где r - это отношение на графе, а⁺ его транзитивное замыкание. Хотя можно представить себе язык спецификации, поддерживающий эти понятия, большинство языков этого не делают.

Все это создает больше трудностей для программиста, которому проще написать булеву функцию cyclic, исследующую граф и возвращающую true, если и только если в графе есть цикл. Такие примеры являются серьезными аргументами в пользу базисного языка утверждений с использованием функций для повышения его выразительной силы.

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

Это неформальное требование достаточно ясно на практике; формализм подъязыка IFL исключает все императивные элементы, которые либо изменяют глобальное состояние системы, либо не имеют тривиальных аппликативных эквивалентов, в частности исключаются:

[x]. присваивания атрибутам;

[x]. присваивания в циклах;

[x]. вызовы программ, не входящих в IFL.

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

Некоторые технические вопросы могут потребовать внимания. Функция f, используемая в утверждении программы r, может сама иметь утверждения, что демонстрируют примеры функций full и correct_index. Возникает потенциальная проблема при мониторинге утверждений в период выполнения: если при вызове r мы вычисляем утверждение, вызывающее f, то не придется ли нам вычислять утверждение для f? Нетрудно сконструировать пример зацикливания, если пойти по этому пути. Но даже и без этого риска было бы неправильно вычислять утверждение для f. Это бы означало, что мы рассматриваем "на равных" программы, являющиеся предметом наших вычислений, такие как r, и их функции утверждения, такие как f. В противовес этому сформулируем правило, согласно которому утверждения должны иметь более высокий приоритет, чем программы, которые они защищают, их корректность должна быть кристально ясной. Правило простое:

Правило вычисления утверждения

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

Если вызов f встречается как часть проверки утверждения программы r, то слишком поздно спрашивать, удовлетворяет ли f своим утверждениям. Подходящим является время, когда решается вопрос использования f в утверждении, применимом к r.

Рассматривайте f как охранника ядерного предприятия, в обязанности которого входит проверка посетителей. Охранников тоже нужно проверять, но не тогда, когда они сопровождают посетителей.

ОО-модель, разрабатываемая до сих пор, включала два частично не связанных аспекта, оба из которых полезны:

[x]. Понятие инварианта класса, введенное в этой лекции.

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

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

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

1 Каждая из m процедур создания порождает объект, удовлетворяющий INV.

2 Каждая из n экспортируемых программ сохраняет INV.

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

Это неформальное доказательство, однако, не верно в присутствии семантики ссылок и динамических псевдонимов. Проблема в том, что атрибуты объекта могут модифицироваться операциями другого объекта. Даже если a.r сохраняет INV для объекта ОА, присоединенного к а, то некоторая операция b.s (для b, присоединенного к другому объекту,) может разрушить INV для ОА. Так что условия (1) и (2) могут выполняться, но INV может не быть инвариантом.

Вот простой пример. Предположим, что А и В классы, каждый из которых содержит атрибут другого класса:

class A ... feature forward: B ... end

class B ... feature backward: A ... end

Потребуем, чтобы ссылки были связаны содержательным условием. Если ссылка forward определена и задает экземпляр класса В, то ссылка backward этого экземпляра, в свою очередь, должна указывать на соответствующий экземпляр класса А. Это может быть выражено как инвариант класса А:

round_trip: (forward /= Void) implies (forward.backward = Current)

Вот пример ситуации, включающей экземпляры обоих классов и удовлетворяющей инварианту:

Рис. 11.9.  Согласованность ссылок forward и backward

Инвариант round_trip встречается в классах довольно часто. Например, в роли класса А может выступать класс PERSON, характеризующий персону. Ссылка forward может указывать в этом случае на владение персоны - объект класса HOUSE. Ссылка backward в этом классе указывает на владельца дома. Еще одним примером может быть реализация динамической структуры - дерева, узел которого содержит ссылки на старшего сына и на родителя. Для этого класса можно ввести инвариант в стиле round_trip:

Предположим, что инвариант класса В, если он есть, ничего не говорит об атрибуте backward. Следующая версия класса А по-прежнему имеет инвариант:

class A feature

forward: B

attach (b1: B) is

-- Ссылка b1 на текущий объект.

do

forward := b1

-- Обновить ссылку backward объекта b1 для согласованности:

if b1 /= Void then

b1.attach (Current)

end

end

invariant

round_trip: (forward /= Void) implies (forward.backward = Current)

end

Вызов b1.attach восстанавливает инвариант после обновления forward. Класс В должен обеспечить свою собственную процедуру attach:

class B feature

backward: B

attach (a1: A) is

-- Ссылка a1 на текущий объект.

do

backward := a1

end

end

Класс А сделал все для своей корректности: процедура создания по умолчанию гарантирует выполнение инварианта, так как устанавливает forward равным void, а его единственная процедура гарантирует истинность инварианта. Но рассмотрим выполнение у клиента следующей программы:

a1: A; b1: B

...

create a1; create b1

a1.attach (b1)

b1.attach (Void)

Вот ситуация после выполнения последней инструкции:

Рис. 11.10.  Нарушение инварианта

Инвариант для ОА нарушен. Этот объект теперь указывает на ОВ, но ОВ не указывает на ОА, - backward равно void. Вызов b1.attach мог связать ОВ с любым другим объектом класса А и это тоже было бы некорректно.

Что случилось? Динамические псевдонимы вновь себя проявили. Приведенное доказательство корректности класса А правильно, и единственная процедура этого класса attach спроектирована в полном соответствии с замыслом. Но этого недостаточно для сохранения согласованности ОА, так как свойства ОА могут включать экземпляры других классов, а доказательство ничего не говорит об эффекте, производимом свойствами других классов на инвариант из А.

Эта проблема достаточно важна, и заслуживает собственного имени: Непрямой Эффект Инварианта (Indirect Invariant Effect). Он может возникать сразу же при допущении динамических псевдонимов, благодаря которому операции могут модифицировать объекты даже без включения любой связанной сущности. Но мы уже видели, как много пользы приносят динамические псевдонимы; и схема forward - backward далеко не академический пример, это, как отмечалось, полезный образец для практических приложений и библиотек.

Что можно сделать? Промежуточный ответ включает соглашения для мониторинга утверждений в период выполнения. Вы, возможно, удивлялись, почему эффект включения мониторинга утверждений на уровне assertion (invariant) был описан так:

"Проверка выполнимости инвариантов класса на входе и выходе программы для квалифицированных вызовов".

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

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

trip_round: (backward /= Void) implies (backward.forward = Current)

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

Еще не все сделано с Проектированием по контракту. Предстоит изучить два важных следствия рассмотренных принципов:

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

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

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

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

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

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

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

[x]. Класс описывает одну возможную реализацию АТД; отображение класса в АТД выражается функцией абстракции, обычно частичной. Обратное отношение, обычно, не задается функцией.

[x]. Инвариант реализации, - часть инварианта класса - выражает корректность представления классом соответствующего АТД.

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

[x]. Если класс поставляется с утверждениями, то можно формально определить, что означает корректность класса.

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

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

[x]. Комбинация инвариантов и динамических псевдонимов приводит к Непрямому Эффекту Инварианта, который может стать причиной нарушения инварианта при корректности самого класса.

Из работы Тони Хоара [Hoare 1981]:

Понятие утверждения, представленное в этой лекции, восходит к работам по корректности программ, пионерами которых были Боб Флойд [Floyd 1967], Тони Хоар [Hoare 1969], Эдсгар Дейкстра [Dijkstra 1976], в дальнейшем описанные в [Gries 1981]. Книга "Введение в теорию языков программирования" (Introduction to the Theory of Programming Languages) [M 1990] представляет обзор этого направления.

Понятие инварианта класса пришло из Хоаровской работы [Hoare 1972a] по инвариантам типов данных. Смотри также приложения к проектированию программ в [Jones 1980], [Jones 1986]. Формальная теория морфизмов между АТД типами может быть найдена у [Goguen 1978].

Библиографические ссылки по формальным языкам спецификаций, включая Z, VDM, OBJ-2, Larch, можно найти в лекции 6. В работе [Lano 1994] , содержащей большое число ссылок, описаны ОО-формальные языки спецификаций, включая Object Z, Z++, MooZ, OOZE, SmallVDM, VDM++.

Стандарты по терминологии программных ошибок, дефектов, неисправностей опубликованы IEEE Computer Society [IEEE 1990], [IEEE1993]. Их Web-страница - http://www.computer.org

Удивительно, но немногие языки программирования поддерживают синтаксическую поддержку утверждений. Ранним примером (первым, который стал мне известен) был язык AlgolW, созданный Хоаром и Виртом [Hoare 1966], непосредственный предшественник языка Pascal. Другие включают Alphard [Shaw 1981] и Euclid [Lampson 1977], спроектированные специально для разработки корректных программ. Связь с ОО-разработкой и нотация, введенная в этой книге, навеяна утверждениями языка CLU [Liskov 1981], который никогда не был реализован. Другая, базирующаяся на CLU книга Лискова и Гуттага [Liskov 1986] является одной из немногих книг по методологии программирования, в которой глубоко обсуждаются вопросы разработки надежного ПО, предлагая подход на базе "защитного программирования", подвергнутый критике в данной лекции.

Понятие Программирования по контракту, представленное в этой лекции и разрабатываемое в оставшейся части книги, пришло из [M 1987a], продолженное в работах [M 1988], [M1989c], [M 1992a]. В работе [M 1994a] обсуждаются толерантный и требовательный подходы к проектированию предусловий, обращая особое внимание на применение этих подходов к проектированию повторно используемых библиотек, включая политику "требовательной любви". Дальнейший вклад в развитие этих идей был сделан Джеймсом Мак-Кимом [McKim 1995], [McKim 1996], [McKim 1996a], а также [Henderson-Sellers], который занимался исследованием позиции поставщика ПО.

Напишите спецификацию АТД для класса COMPLEX, описывающую понятие комплексных чисел с арифметическими операциями. Исходите из точной арифметики.

Проверьте все предусловия и аксиомы АТД STACK, введенного в предыдущих лекциях, и покажите, отображаются ли они в классе STACK4, а если да, то как.

Покажите, что введение закрытой функции body, возвращающей тело стека, сделает возможным утверждениям класса STACK полностью отражать спецификацию соответствующего АТД. Обсудите теоретическую и практическую значимость такого подхода.

Почему capacity экспортируется для реализации стеков ограниченных размеров, класс STACK2?

Напишите инвариант реализации для класса STACK3.

Обсудите использование функций в утверждениях, в частности, введение функции correct_index в предусловия программ put и item. Если добавить эту функцию в класс ARRAY, то какой статус экспорта следует ей дать?

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

В этой лекции было показано, что нарушение предусловия указывает на ошибку клиента, а нарушение постусловия указывает на ошибку поставщика. Объясните, почему нарушение инварианта также указывает на ошибку поставщика.

Напишите класс, реализующий алгоритм получения псевдослучайных чисел, основанный на последовательности: n_i = f(n_{i - 1}), где функция f задана, а начальное значение n₀ определяется клиентом класса. Функция не должна иметь побочных эффектов. Определение функции f можно найти в учебниках, таких как [Knuth 1981] и в библиотеках по численным методам.

Напишите класс, реализующий очередь (стратегию доступа "первый пришел - первый ушел", FIFO - "first in - first out"). Задайте подходящие утверждения в стиле класса STACK этой лекции.

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

Когда первое издание этой книги было опубликовано, Европейское Космическое Агентство опубликовало отчет международного исследования тестирования полета космической ракеты Ариан 5, потерпевшей катастрофу 4 июня 1996 года через 40 секунд после старта, по отчету стоившего 500 миллионов долларов (незастрахованного запуска).

Причина катастрофы: ошибки в бортовой компьютерной системе. Причина этой ошибки: преобразование числа с плавающей точкой, представленного 64 битами, в 16-и битовое знаковое целое привело к выбрасыванию исключения. Число задавало горизонтальный наклон (horizontal bias) ракеты. Некоторые исключения в системе обрабатывались, используя механизмы языка ADA, описанные в следующей лекции. Но это исключение не обрабатывалось, поскольку ранее проведенный анализ показал, что оно не может встречаться, поэтому решено было не загромождать код обработчиком соответствующего исключения.

Реальная причина: недостаточная спецификация. Проведенный анализ был вполне корректен, - но для траектории полета ракеты Ариан 4. Программный код был повторно использован при полете ракеты Ариан 5, и предположения, хотя и оставленные в маловразумительной документации, были просто забыты. Их просто не применяли к Ариан 5. При Проектировании по контракту было бы задано предусловие:

require

horizontal_bias <= Maximum_horizontal_bias

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

Урок ясен: повторное использование без контрактов безрассудно. Абстрактные модули, определенные нами, как единицы повторного использования, должны поставляться с ясными спецификациями условий их применения - предусловиями, постусловиями, инвариантами. Эти спецификации должны находиться не во внешних документах, а быть частью самих модулей. Эти принципы, которые мы изучили, особенно Проектирование по контракту и Самодокументирование являются необходимым условием любой успешной политики повторного использования. Даже если ошибки будут стоить менее полумиллиарда долларов, всегда помните об этих правилах:

[x]. Повторно используемый модуль должен быть специфицирован.

[x]. Язык программирования должен поддерживать механизм утверждений.

[x]. Спецификации являются частью самого ПО.

Примечания:

общий класс, описывающий стекиобщий класс, описывающий стеки 11.1

Для инвариантов ответ такой же, как и для постусловийДля инвариантов ответ такой же, как и для постусловий 11.2