Технические приемы, введенные в предыдущих лекциях, были направлены на создание надежного ПО. Дадим их краткий обзор - было бы бесполезно рассматривать более продвинутые концепции до приведения в порядок основных механизмов надежности. Первым и определяющим свойством объектной технологии является почти навязываемая структура программной системы - простая, модульная, расширяемая, - проще гарантирующая надежность, чем в случае "кривых" структур, возникающих при применении ранних методов разработки. В частности, усилия по ограничению межмодульного взаимодействия, сведения его к минимуму, были в центре дискуссии о модульности. Результатом стал запрет общих рисков, снижающих надежность, - отказ от глобальных переменных, механизм ограниченного взаимодействия модулей, отношения наследования и вложенности. Общее наблюдение: самый большой враг надежности (и качества ПО в целом) - это сложность. Создавая наши структуры настолько простыми, сколь это возможно, мы достигаем необходимого, но не достаточного условия, гарантирующего надежность. Прежнее обсуждение служит лишь верной отправной точкой в последующих систематических усилиях.
Заметьте, необходим, но также недостаточен, постоянный акцент на создание элегантного и читабельного ПО. Программные тексты не только пишутся, они еще читаются и переписываются по много раз. Ясность и простота нотации языковых конструкций - основа любого изощренного подхода к надежности.
Еще одно необходимое оружие - автоматическое управление памятью, в особенности сборка мусора. В лекции, посвященной этой теме, в деталях пояснено, почему для любой системы, оперирующей динамическими структурами данных, столь опасно опираться на управление этим процессом вручную. Сборка мусора не роскошь - это ключевой компонент ОО-среды, обеспечивающий надежность.
Тоже можно сказать об еще одном, сочетающемся с параметризацией механизме, - статической типизации. Без правил строгой статической типизации пришлось бы лишь надеяться на снисхождение многочисленных ошибок, возникающих в период выполнения.
Все эти механизмы дают необходимую основу для более полного взгляда на то, что следует предпринять для обеспечения устойчивости и корректности ПО.
Из работы Тони Хоара [Hoare 1981]:
Первым защитником использования утверждений в программировании был никто иной, как сам Алан Тьюринг. На конференции в Кембридже 24 июня 1950 г. он представил небольшой доклад "Проверка больших программ", в которой объяснял эту идею с большой ясностью. "Как можно проверить большую программу, утверждая, что она правильна? Чтобы для проверяющего задача не была слишком трудной, программист обязан написать некоторые утверждения, которые можно проверить индивидуально, и из которых корректность программы следует достаточно просто." |
Понятие утверждения, представленное в этой лекции, восходит к работам по корректности программ, пионерами которых были Боб Флойд [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], который занимался исследованием позиции поставщика ПО.
Еще не все сделано с Проектированием по контракту. Предстоит изучить два важных следствия рассмотренных принципов:
Как они приводят к механизму дисциплинированной обработки исключений; это тема следующей лекции.Как они комбинируются с наследованием, позволяя нам указать, что любые семантические ограничения, применимые к классу, применимы также и к его потомкам; и что семантические ограничения, применимые к компоненту, применимы и при возможных его переопределениях. Эта тема будет изучаться при рассмотрении наследования.
Обобщая, утверждения и Проектирование по контракту будут сопровождать нас во всей оставшейся части этой книги, позволяя проверить, знаем ли мы, что делают создаваемые нами элементы.
Синтаксически инвариант класса является утверждением, появляющимся в предложении 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 это множество утверждений, которым удовлетворяет каждый экземпляр класса во все "стабильные" времена. В эти времена экземпляр класса находится в наблюдаемом состоянии:
на момент создания экземпляра, сразу после выполнения create a или create a.make(...), где a класса C;перед и после каждого удаленного вызова a.r(...) программы r класса С.
Следующий рисунок, показывающий жизнь объектов, поможет разобраться в инвариантах и стабильных временах:
Жизнь объектов не столь уж захватывающая. Вначале - слева на рисунке - он просто не существует. При выполнении инструкции create a или create a.make(...) или clone объект создается и достигает первой станции S1 в своей жизни. Затем идет череда довольно скучных событий: клиенты, для которых доступен объект, один за другим вызывают его компоненты в форме a.f(..). Так все продолжается, пока не завершится вычисление.
Инвариант является характеристическим свойством состояний, представленных большими квадратиками на рисунке: S1, S2, S3 и т.д. Эти состояния соответствуют стабильным временам, упомянутым выше.
Здесь рассматриваются последовательные вычисления, но все идеи легко переносятся на параллельные вычисления, что и будет сделано в соответствующей лекции. |
Пусть А - это некоторая операция (оператор или тело программы). Формула корректности (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}
Число 13 в постусловии не опечатка. Предполагая корректную реализацию целочисленной арифметики, данная формула действительно выполняется. Если предусловие x>=9 выполняется перед присваиванием, то x>=13 будет истинным по завершении оператора присваивания. Конечно, можно утверждать более интересную вещь: при заданном предусловии сильнейшим, насколько это возможно, будет постусловие x>=14. В свою очередь, при заданном постусловии x>=13 слабейшим предусловием будет x>=8. Из выполняемой формулы корректности всегда можно породить новые выполняемые формулы, ослабляя постусловие или усиливая предусловие. Займемся теперь выяснением того, что означают термины "сильнее" и "слабее" в пред- и постусловиях. |
Этот раздел требует от читателя определенной математической подготовки.
Полезно рассмотреть предшествующее обсуждение в терминах следующего рисунка, навеянного работой [Hoare 1972a], в которой описывается понятие "С является корректной реализацией А".
Здесь А - АТД, С - класс, его реализующий. Абстрактной функции 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. Результат будет одним и тем же, если:
Применить конкретную функцию класса cf, а потом функцию абстракции а, получив a(cf(CONC_1)).Применить функцию абстракции а, а потом функцию АТД - af, получив af(a(CONC_1)).
Утверждения из STACK2 иллюстрируют фундаментальную концепцию - разницу между императивным и аппликативным видением.
Утверждения empty и full могут вызвать удивление. Приведу еще раз текст full:
full: BOOLEAN is -- Заполнен ли стек? do Result := (count = capacity) ensure full_definition: Result = (count = capacity) end
Постусловие говорит, что Result имеет значение выражения (count = capacity). Но оператор присваивания именно это значение присваивает переменой Result. В чем же смысл написания постусловия? Не является ли оно избыточным?
Фактически между двумя конструкциями большая разница. Присваивание это команда, отданная виртуальному компьютеру на изменение его состояния. Утверждение ничего не делает, оно специфицирует свойство ожидаемого заключительного состояния, полученное клиентом, вызвавшим программу.
Инструкция предписывает (prescriptive), утверждение описывает (descriptive). Инструкция описывает "как", утверждение описывает "что". Инструкция является частью реализации, утверждение - элементом спецификации.
Инструкция императивна, утверждение - аппликативно. Эти два термина выражают фундаментальную разницу между программированием и математикой.
Компьютерные операции могут изменять состояние аппаратно-программной машины. Инструкции в языках программирования являются командами (императивные конструкции), заставляющие машину выполнять такие операции.Математические вычисления никогда ничего не меняют. Как отмечалось при рассмотрении АТД, взятие квадратного корня от числа 2 не меняет это число. Вместо этого математики описывают как, используя свойства одних объектов, вывести свойства других, таких как v2, полученных применением (applying - отсюда и термин "аппликативный") математических трансформаций.
То, что две нотации в нашем примере так близки, - присваивание и эквивалентность - не должно затемнять фундаментальное различие. Утверждение описывает ожидаемый результат, инструкция предписывает способ его достижения. Клиенты модуля обычно интересуются утверждениями, а не реализациями.
Реализация | Спецификация |
Инструкция | Выражение |
Как | Что |
Императив | Аппликатив |
Предписание | Описание |
Простой пример вычисления максимума массива иллюстрирует общую схему циклических вычислений, применимую ко многим ситуациям. Вы определяете, что решением некоторой проблемы является элемент, принадлежащий n-мерной поверхности POST. В некоторых случаях POST может содержать ровно один элемент - решение, но обычно может быть более чем одно приемлемое решение проблемы. Циклы полезны, когда нет прямого способа достичь решения "одним выстрелом". Но у вас есть непрямая стратегия, вы можете, например, прицелиться и попасть в m-мерную поверхность INV, включающую POST (для m>n). Инвариантом является то, что поверхность попадания все время содержит POST. Итерация за итерацией приближаемся к POST, сохраняя истинность INV. Следующий рисунок иллюстрирует этот процесс:
Вычисление цикла имеет следующие ингредиенты:
Цель post, определяемую как свойство, выполняемое в любом допустимом заключительном состоянии. Пример: "Result является максимумом массива". На рисунке цель post представлена множеством состояний POST.Инвариант цикла inv, являющийся обобщением цели, так что можно говорить, что цель - это частный случай инварианта. Пример: "Result является максимумом текущей нарезки массива". Инвариант цикла поиска цели, изображенный на рисунке: "Каждая точка лежит на поверхности, содержащей POST.Точку инициализации init, о которой известно, что она должна быть в INV, другими словами должна обеспечить выполнение инварианта.Преобразование body, начинающееся в INV, но не в POST, вырабатывающее точку более близкую к POST, но все еще остающуюся в INV. Тело цикла функции maxarray является примером подобного преобразования.Верхняя граница числа применений body, необходимого для перевода точки из INV в POST. Как будет пояснено ниже, этот параметр необходим для определения варианта.
Последовательные приближения один из главных инструментов численного анализа. Но там эта идея понимается шире. Важная разница состоит в том, что в чистой математике допускаются бесконечные вычисления, последовательность может иметь предел, даже если он не достигается конечным числом приближений.
Утверждения, рассматриваемые до сих пор - предусловия, постусловия, инварианты, - это основные составляющие метода. Они устанавливают связь между конструкциями ОО-программных систем и теорией АТД, лежащей в основе метода. Инварианты класса, в частности, не могут быть поняты, и даже обсуждаться вне рамок ОО-подхода.
Можно рассматривать и другие возможности использования утверждений. Хотя они менее специфичны для нашего метода, но тоже играет важную роль, и должны быть частью нашей нотации. Наши расширения будут включать инструкцию проверки 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 помогает избежать подобных проблем, требуя документирования нетривиальных предположений.
Механизмы утверждений, рассмотренные в этой лекции, помимо того, что они дают преимущества все вещи делать правильно с самого начала, они еще позволяют найти то, что сделано неверно. Используя параметры компиляции можно включить проверку, и сделать инструкцию check реально проверяемой в период выполнения. Если все предположения выполняются, то проверка не оказывает воздействия на процесс вычислений, но, если вы ошиблись, и предположения не выполняются, то в точке их нарушения будет выброшено исключение и процесс остановится. Тем самым появляется возможность быстрого обнаружения содержательных ошибок. Механизм checking - включения проверок будет вкратце рассмотрен в дальнейшем. |
Возможно, вы не заметили, что контракт противоречит мудрости, бытующей в программной инженерии. Поначалу это шокирует, но контракт - один из главных вкладов в надежность ПО.
Правило контракта говорит, что предусловие дает преимущество поставщику, если клиентская часть контракта не выполняется, то класс перестает быть связан постусловием. В этом случае программа может делать все что угодно, например зациклиться, не нарушая при этом контракт. Это тот самый случай, когда "заказчик виноват".
Первое преимущество от такого соглашения в том, что стиль программирования существенно упрощается. Разработчик класса при написании тела программы смело может предполагать, что все ограничения, заданные предусловием, выполняются; ему нет нужды проверять их в теле программы. Так для функции, вычисляющей квадратный корень:
sqrt (x: REAL): REAL is -- Квадратный корень из x require x >= 0 do ... end
можно смело применять алгоритм, не учитывающий случай отрицательного x, поскольку это предусмотрено предусловием, и ответственность за его выполнение несут клиенты программы. С первого взгляда это может показаться опасным, но читайте дальше. Фактически метод Проектирования по Контракту идет дальше. Предположим, что мы написали в предложении do предыдущей программы следующий текст:
if x < 0 then "Обработать ошибку как-нибудь" else "Выполнить нормальное вычисление квадратного корня" end
Заметьте, в этом не только нет никакой необходимости, но это и неприемлемо! Этот факт можно отразить в следующем методологическом правиле:
Принцип Нет-Избыточности
Ни при каких обстоятельствах в теле программы не должно проверяться ее предусловие
Это правило противоречит тому, чему учат во многих учебниках по программирования, где необходимость проверок часто выступает под знаменами "защитного программирования" (defensive programming). Его идея в том, что для получения надежного ПО каждая программа должна защищать себя настолько, насколько это возможно. Лучше больше проверок, чем недостаточно; нельзя доверять незнакомцам; еще одна проверка может и не поможет, но и не навредит делу.
Следует отметить, что избыточные проверки широко применяются в процессе функционирования компьютеров и другой электронной аппаратуры. Физическая система, нормально функционирующая, со временем может терять целостность; причины разные - износ, разрыв, внешние воздействия. Поэтому нормальной практикой является, когда получатель и отправитель сигнала оба проверяют его целостность. Для программных систем феномена износа не наблюдается, нет и необходимости в избыточных проверках. Можно также заметить, что так называемая избыточная проверка аппаратуры, на самом деле таковой не является: это могут быть различные дополнительные тесты, например, проверка на четность, проверка разных устройств и т.д. |
Несмотря на свое имя, инвариант не должен выполняться во все времена. Вполне законно, что некоторая процедура g, начиная выполнять свою работу, разрушает инвариант, а, завершая работу, восстанавливает его истинность. В промежуточном состоянии, показанном на рисунке маленьким квадратиком, инвариант не выполняется, но инвариант всегда должен выполняться в заключительном состоянии каждой процедуры. И в человеческом сообществе многие, стараясь сделать что-либо полезное, начинают с того, что разрушают существующий порядок вещей.
В метафоре контрактов интерпретация инвариантов ясна и понятна. В сообществе людей все контракты часто содержат ссылки на общие правила, регулирующие отношения между партнерами независимо от конкретной области применения контракта. Например правила, установленные для городских зон, справедливы для всех контрактов по строительству жилья. Инварианты класса играют роль общих правил: инвариант класса действует на все контракты между программами класса и клиентами.
Давайте пойдем дальше. Выше отмечалось, что инварианты можно рассматривать как добавки к предусловиям и постусловиям экспортируемых программ. Пусть body тело программы, pre - предусловие, post - постусловие, Inv - инвариант программы. Требование корректности программы может быть записано в виде:
{INV and pre} body {INV and post}
Это означает, что любое выполнение body, начинающееся в состоянии, удовлетворяющем Inv и pre, завершится в состоянии, в котором выполняются Inv и post. Для человека, создающего body, появление инварианта является "хорошей" или "плохой" новостью, облегчается или затрудняется его задача? Ответ, как следует из предыдущих обсуждений, и да и нет! Вспомним ленивого работника, который мечтает о сильном предусловии и слабом постусловии, чтобы можно было бы работать как можно меньше. Инвариант усиливает как предусловие, так и постусловие. Так что, если вы ответственны за реализацию body, то добавление инварианта:
Облегчает работу: накладывая на клиента более жесткие требования, уменьшая тем самым число ситуаций, при которых нужно приступать к работе.Усложняет работу: помимо постусловия в заключительном состоянии необходимо гарантировать выполнение инварианта.
Эти наблюдения согласуются с ролью инварианта, задающего общие требования к классу. Приступая к работе над одной из программ класса, вы получаете преимущества, поскольку гарантируется выполнение общих для класса условий. Но на вас возлагается обязанность к концу работы сохранить выполнимость этих условий, чтобы ими могли воспользоваться и другие программы класса.
Заметьте, balance может быть не атрибутом, а функцией, возвращающей значение, вычисляемое, например, так: deposits_list.total - withdrawal_list.total. В этом случае процедуре withdraw вообще ничего не нужно делать для обеспечения выполнимости инварианта. Возможность переключаться между двумя представлениями (атрибута и функции) без влияния на клиента обеспечивается принципом Унифицированного доступа. |
Наши следующие и последние конструкции утверждений помогут строить корректные циклы. Эти конструкции являются прекрасным дополнением рассмотренных ранее механизмов. Поскольку они не являются специфической частью ОО-метода, то вы вправе пропустить этот раздел при первом чтении.
Предусловия и постусловия описывают свойства отдельных программ. Но экземпляры класса обладают также глобальными свойствами. Их принято называть инвариантами класса (class invariants), и они определяют более глубокие семантические свойства и ограничения целостности, характеризующие класс.
ОО-модель, разрабатываемая до сих пор, включала два частично не связанных аспекта, оба из которых полезны:
Понятие инварианта класса, введенное в этой лекции.Гибкая модель периода выполнения, детально рассмотренная в начальных лекциях, существенно использующая ссылки.
К несчастью, эти индивидуально желательные свойства могут стать причиной трудностей при их совместном использовании.
Проблема вновь в динамически создаваемых псевдонимах, предохраняющих нас от проверки корректности класса на том основании, что класс делает это сам. Мы уже видели, что корректность класса означает проверку m+n свойств, выражающих следующее (если мы концентрируем внимание на инвариантах INV, игнорируя предусловия и постусловия, не играющие здесь роли):
Каждая из m процедур создания порождает объект, удовлетворяющий INV.Каждая из 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 этого экземпляра, в свою очередь, должна указывать на соответствующий экземпляр класса А. Это может быть выражено как инвариант класса А:
Некоторые утверждения появляются в реализации, хотя они не имеют прямых двойников в спецификации АТД. Эти утверждения используют атрибуты, включая некоторые закрытые атрибуты, которые, по определению, не имеют смысла в АТД. Простым примером являются свойства, появляющиеся в инварианте 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.
Теперь мы уже познакомились со всеми конструкциями, содержащими утверждения. Разумно, еще раз взглянуть на те преимущества, которые мы можем получить от этого. Выделим четыре основных применения.
Помощь в создании корректного ПО.Поддержка документирования.Поддержка тестирования, отладки и гарантия качества.Поддержка приемлемого способа обработки неисправностей.
Только два последних пункта предполагают мониторинг утверждений в период выполнения.
Второе использование является основным в производстве повторно используемых программных элементов и, более обще, в организации интерфейсов модулей в большой программной системе. Постусловия, предусловия, инварианты классов обеспечивают потенциальных клиентов модуля необходимой информацией о предлагаемых модулем службах, выраженной в соответствующей и точной форме. Никакое количество описательной документации не может заменить множества аккуратно выраженных утверждений, являющихся частью самого ПО.
В самом последнем разделе этой лекции можно ознакомиться с проектом, где эти правила были проигнорированы, что обошлось в $500 миллионов и привело к провалу космического проекта. |
Средство автоматической документации 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. Хотя достаточно просто превратить эту форму в правильный отложенный класс, известное понятие, рассматриваемое в деталях при изучении наследования.
В среде ISE получить краткую форму можно одним щелчком соответствующей кнопки в Class Tool; можно генерировать либо плоский текст, либо текст в форматах HTML, RTF, MML (FrameMaker), TEX и других. Можно определить и свой собственный формат. |
Каков уровень трассировки следует включать? Ответ вырабатывается в результате компромисса, с учетом следующих факторов: уровня доверия к корректности ПО, насколько критичны потери эффективности, насколько серьезны последствия не обнаруженных ошибок в период выполнения.
В экстремальных ситуациях все ясно:
При тестировании системы или очередной ее версии следует включать на самом высоком уровне мониторинг классов (для используемых библиотек это не обязательно). Эта возможность - один из принципиальных вкладов метода, представленного в этой книге. Мало кто из людей осознавал мощь этих идей, и как основательно они влияют на практику разработки ПО. Перелом наступил, когда фактически был получен опыт тестирования больших систем с утверждениями, включающих механизм мониторинга, описанный в этом разделе.Для системы с полной степенью доверия в приложениях, критичных по времени выполнения, где каждая микросекунда на счету, - следует полностью удалять мониторинг.
Последний совет парадоксален, при отсутствии формальных доказательств корректности говорить о "полной степени доверия" вряд ли возможно. Стоит привести красноречивое высказывание C. A. Hoare:
Абсурдно выполнять проверку в период отладки, когда не требуется доверие к получаемым результатам, и отключать ее в рабочем состоянии, когда ошибочный результат может стоить дорого или вообще катастрофичен. Что бы вы подумали о любителе плавания, который надевает спас-жилет во время тренировок на берегу и снимает его, бросаясь в море [Hoare 1973]. |
Интересную возможность дает параметр, включающий проверку предусловий. В рабочем режиме, когда отладка завершена и даны гарантии качества, крайне важно избежать катастроф в результате необнаруженных вызовов программ вне области их применения. Эта проверка обходится намного дешевле, чем проверка постусловий и инвариантов. Инварианты, в частности, особенно дороги, поскольку они проверяются на входе и выходе каждого квалифицированного вызова, и, что более важно, они всегда сложны, поскольку включают условия согласованности компонент класса.
В нашем компиляторе каждое вхождение каждого индекса в каждый массив проверялось во всех случаях в период выполнения. Через много лет мы спросили наших клиентов, не стоит ли ввести в интересах эффективности параметр компиляции, позволяющий отключать эту проверку. Единогласно они убеждали нас, не делать этого, - они уже хорошо знали, как часто встречается эта ошибка и к каким ужасным последствиям она может приводить. Со страхом и ужасом я заметил, что даже сегодня проектировщики языков и пользователи не выучили этот урок. В любой уважающей себя ветви инженерии непринятие предосторожностей такого рода считались бы нарушением закона. |
Как бы ни были необходимы компромиссы между факторами качества, один из факторов стоит в стороне от остальных - корректность. Нет никакого оправдания тому, что корректность подвергается опасности ради других факторов, таких как эффективность. Если программный продукт не выполняет свою функцию, все остальное не имеет смысла. |
Этот пример даст возможность ознакомиться с практическим использованием утверждений. В предыдущей лекции была дана схема параметризованного класса "стек" в форме:
class STACK [G] feature ... Объявление компонент: count, empty, full, put, remove, item end
Реализация появится ниже. До рассмотрения проблем реализации важно отметить, что программы характеризуются строгими семантическими свойствами, не зависящими от специфики реализации. Например:
Программы remove и item применимы, только если число элементов стека не равно нулю.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.
Обратите внимание на разделы feature, группирующие свойства по категориям, снабженных заголовками в виде комментариев. Категории Access, Status report, Element change - это несколько примеров из десятков стандартных категорий, используемых в библиотеках и применяемых повсеместно в примерах этой книги. |
Утверждения - это булевы выражения, задающие семантические свойства класса и вводящие аксиомы и предусловия соответствующего абстрактного типа данных.Утверждения используются в предусловиях (требования, при выполнении которых программы применимы), постусловиях (свойства, гарантируемые на выходе программ), и инвариантах класса (свойства, характеризующие экземпляры класса во время их жизни). Другими конструкциями, включающими утверждения, являются инварианты цикла и инструкции check.Предусловие и постусловие программы описывают контракт между программой и ее клиентами. Контракт связывает программу, только при условии ее вызова, в состоянии, где предусловие выполняется; в этом случае программа гарантирует выполнимость постусловия на выходе. Понятие заключения контрактов между программами обеспечивает мощную метафору при построении надежного ПО.Инвариант класса выражает семантические ограничения экземпляров класса. Инвариант неявно добавляется к предусловиям и постусловиям каждой экспортируемой программы класса.Класс описывает одну возможную реализацию АТД; отображение класса в АТД выражается функцией абстракции, обычно частичной. Обратное отношение, обычно, не задается функцией.Инвариант реализации, - часть инварианта класса - выражает корректность представления классом соответствующего АТД.Цикл может иметь инвариант цикла, позволяющий вывести результат выполнения цикла, и вариант, позволяющий доказать завершаемость цикла.Если класс поставляется с утверждениями, то можно формально определить, что означает корректность класса.Утверждения служат четырем целям: помогают в конструировании корректных программ; помогают в создании документации, помогают в отладке, являются основой механизма исключений.Язык утверждений в нашей нотации не включает логику предикатов первого порядка, но может выражать многие свойства высокого уровня благодаря вызову функций. Функции, включаемые в утверждения должны быть простыми и безупречно корректными.Комбинация инвариантов и динамических псевдонимов приводит к Непрямому Эффекту Инварианта, который может стать причиной нарушения инварианта при корректности самого класса.
Хотя нам еще предстоит ознакомиться с рядом конструкций, связанных с утверждениями, пора сделать паузу и проэкзаменовать некоторые из следствий уже изученных понятий - предусловий, постусловий, инвариантов. В этом разделе не вводятся никакие новые конструкции, но описываются теоретические обоснования сделанного. Полагаю, и при первом чтении следует познакомиться с этими идеями, поскольку они являются основополагающими для правильного понимания метода, и будут иметь большую ценность при попытке постигнуть, как использовать наследование должным образом.
Для понимания отношений между утверждениями и АТД необходимо, прежде всего, установить отношение между компонентами класса и их двойниками - АТД функциями. В свете прежних обсуждений функции подразделяются на три категории: создатели, запросы и команды. Возвращаясь назад, напомню, категория функции f
f : A ? B ? ...
Xзависит от того, где имя АТД, скажем T, встречается среди типов A, B, ... X, включенных в эту сигнатуру:
Если Т появляется только справа от стрелки, f является создателем; в классе это соответствует процедуре создания.Если Т появляется только слева от стрелки, f является запросом, обеспечивающим доступ к свойству экземпляра класса. Для класса запрос соответствует атрибуту или функции; термин запрос сохраняется и для класса, когда нет необходимости различать, как он реализован.Если Т появляется как слева, так и справа от стрелки, f является командой, вырабатывающей новый объект из одного или нескольких уже существующих. На этапе реализации f часто задается процедурой (также называемой командой), которая модифицирует существующий объект, не создавая новый, как это делают функции.
Предусловие и постусловие программы определяют контракт со всеми ее клиентами.
Вооруженные понятиями инварианта, предусловий и постусловий, мы можем теперь точно определить понятие корректности уже не отдельной подпрограммы, а класса в целом.
Класс, подобно всем остальным программным элементам, не может быть корректным или некорректным сам по себе, - только по отношению к некоторой спецификации. Инварианты, предусловия и постусловия, это способ задания спецификации класса. На этой основе можно приступать к определению корректности: класс корректен, если и только если его реализация, заданная подпрограммами, согласована с предусловиями, постусловиями и инвариантами.
Нотация {P} A {Q} поможет выразить наше определение более строго.
Пусть C обозначает класс, Inv - инвариант, r - программа класса. Для каждой программы Bodyr - ее тело, prer(xr), postr(xr) - ее предусловие и постусловие с возможными аргументами xr. Если предусловие или постусловие для программы r опущены, то будем считать их заданными константой True.
Наконец, пусть DefaultC обозначает утверждение, выражающее тот факт, что атрибуты класса C имеют значения по умолчанию, определенные их типами. Например, DefaultSTACK2 для класса STACK2 является следующим утверждением:
representation = Void capacity = 0 count = 0
Эта нотация позволяет дать общее определение корректности класса:
Определение: Корректность класса
Класс C корректен по отношению к своим утверждениям, если и только если:
Для любого правильного множества аргументов xp процедуры создания p:
{DefaultC and prep(xp)} Bodyp {postp(xp) and Inv}
Для каждой экспортируемой программы r и для любого множества правильных аргументов xr:
{prer(xr) and Inv} Bodyr {postr(xr) and Inv}
Это правило является математической формулировкой ранее рассмотренной неформальной диаграммы, показывающей жизненный цикл типичного объекта (рис. 11.4). Условие (1) означает, что любая процедура создания при ее вызове с выполняемым предусловием должна вырабатывать начальное состояние (S1 на рисунке), удовлетворяющее постусловию и инварианту. Условие (2) отражает тот факт, что любая экспортируемая процедура r (f и g на рисунке), вызываемая в состояниях (S1, S2, S3), вызываемая в состояниях, удовлетворяющих предусловию и инварианту, должна завершаться в состояниях, удовлетворяющих постусловию и инварианту.
Два практических замечания:
Если у класса нет предложения creation, то можно полагать, что существует неявная процедура создания по умолчанию - nothing с пустым телом. Применение правила (1) к Bnothing в этом случае означает, что DefaultC влечет Inv; другими словами, значения полей по умолчанию должны удовлетворять инварианту в этом случае.Из определения корректности класса следует, что любая экспортируемая программа может делать, все что угодно, если при ее вызове нарушается предусловие или инвариант.
Только что было описано, как определить корректность класса. На практике чаще хочется проверить, что данный класс действительно корректен. Эта проблема будет обсуждаться позднее в этой лекции.
Квалифицированные вызовы в форме a.f(...), выполняемые на стороне клиента, всегда начинаются и заканчиваются в состоянии, удовлетворяющем инварианту. Подобного правила нет для неквалифицированных вызовов в форме f(...), недоступных для клиентов, но используемых в квалифицированных вызовах для служебных целей. Как следствие, обязанность управлять инвариантами возлагается только на модули, экспортируемые всем клиентам или выборочно. Закрытые методы, недоступные клиентам, не обязаны беспокоиться об инвариантах.
Закончим обсуждение правилом, точно определяющим, когда утверждение является корректным инвариантом класса:
Правило инварианта
Утверждение Inv является корректным инвариантом класса, если и только если оно удовлетворяет следующим двум условиям:
Каждая процедура создания, применимая к аргументам, удовлетворяющим ее предусловию в состоянии, в котором атрибуты имеют значения, установленные по умолчанию, вырабатывает заключительное состояние, гарантирующее выполнение Inv.Каждая экспортируемая процедура класса, примененная к аргументам в состоянии, удовлетворяющем Inv и предусловию, вырабатывает заключительное состояние, гарантирующее выполнение Inv.
Заметьте, в этом правиле:
Предполагается, что каждый класс обладает процедурой создания, задаваемой конструктором по умолчанию, при отсутствии явного ее определения.Состояние объекта определяется значениями всех его полей (значениями атрибутов класса для этого конкретного экземпляра).Предусловие программы может включать начальное состояние и аргументы.Постусловие может включать только заключительное состояние, начальное состояние, (используя нотацию old) и, в случае функций, возвращаемое значение, заданное предопределенной сущностью Result.Инвариант может включать только состояние.
Утверждения могут использовать функции, но такие функции фактически являются ссылками на атрибуты - состояние. |
Математическое выражение правила Инварианта появится позже в этой лекции.
Можно использовать правило Инварианта как основу для ответа на вопрос, что означает нарушение инварианта в период выполнения системы? Мы уже установили, что нарушение предусловия означает ошибку (жучок) клиента, нарушение постусловия - ошибка поставщика. Для инвариантов ответ такой же, как и для постусловий2).
Пришло время, дать полный ответ на вопрос: "какой эффект производят утверждения в период выполнения?". Как отмечалось, ответ определяется разработчиком, имеющим возможность управлять параметрами компиляции. Выбор нужных параметров не требует изменения текста класса, вместо этого меняется содержимое Ace файла. Напомню, Ace файл написан на языке Lace, описывающем компиляцию и сборку системы.
Напомню также, что 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(...):
no - не выполнять никакое из утверждений. В этом режиме оказывают на выполнение не больший эффект, чем комментарии;require - только проверка выполнимости предусловий на входе программ;ensure - проверка выполнимости постусловий на выходе из программы;invariant - проверка выполнимости инвариантов класса на входе и выходе программы для квалифицированных вызовов (obj.f);loop - проверка выполнимости инвариантов цикла перед и после каждой итерации; проверка уменьшения вариантов на каждой итерации с сохранением их не отрицательности;check - выполнение предложений check, проверяющих выполнимость соответствующих утверждений.
Как отмечалось в лекции про АТД, они включают четыре элемента:
имя типа, возможно с родовым параметром (раздел TYPES);список функций с их сигнатурами (раздел FUNCTIONS);аксиомы, выражающие свойства результатов функций (раздел AXIOMS);ограничения применимости функций (раздел PRECONDITIONS).
При поверхностном применении АТД часто опускают две последние части. Во многом, это лишает данный подход привлекательности, поскольку предусловия и аксиомы выражают семантические свойства функций. Если их опустить и просто рассматривать стек как инкапсуляцию операций put, remove и других, то преимущества от скрытия информации останутся, но это все. Понятие стека становится пустой оболочкой без семантики, кроме той, что остается в именах функций. (В этой книге имена функций менее информативны по причине согласованности и повторного использования, - мы сознательно выбрали общие имена - put, remove, item, а не те, которые применяются обычно для стеков - push, pop, top).
Этот риск потери семантики переносится на программирование: программы, реализующие операции соответствующего АТД, в принципе могут выполнять нечто отличное от задуманного. Утверждения предотвращают этот риск, возвращая семантику классу.
Действительно, нужно ли проверять утверждения в период выполнения? После того, как мы были в состоянии, используя утверждения, дать теоретическое определение корректности класса: каждая процедура создания должна гарантировать инвариант, и тело каждой процедуры, запущенной в состоянии, удовлетворяющем инварианту и предусловию, сохраняет в заключительном состоянии инвариант и гарантирует выполнение постусловия. Теперь мы должны выполнить математическую проверку m+n соответствующих условий (для m процедур создания и n экспортируемых процедур), и тогда долой мониторинг в период выполнения.
Мы должны, но мы не можем. Доказательство правильности программ уже многие годы является активной областью исследований, и достигло определенных успехов. Все же сегодня невозможно проверить корректность реального ПО, написанного на современных языках программирования.
Для этого необходим, в частности, и более мощный язык утверждений. Язык IFL, обсуждаемый ниже, может быть использован как часть стратегии многоярусного доказательства. |
Даже, если со временем методы и инструментальные средства доказательства станут доступными, можно ожидать, что отказаться от мониторинга не удастся. В системе всегда останется место трудно предсказуемым событиям - ошибкам аппаратуры, ошибкам в самом доказательстве. Поэтому следует применять хорошо известную в инженерии технику - множественные, независимые способы проверки.
Зададимся вопросом, что означает утверждение - программный элемент корректен? Наблюдения и рассуждения, отвечающие на это вопрос, могут показаться тривиальными. Но, как заметил один известный ученый, таковы все научные результаты, - они начинаются с обычных наблюдений и продолжаются путем простых рассуждений, но все это нужно делать упорно и настойчиво.
Предположим, некто пришел к вам с программой из 300 000 строк на С и спрашивает, корректна ли она? Если вы консультант, то взыщите высокую плату и ответьте - "нет". Вы, вероятно, окажетесь правы.
Для того чтобы можно было дать разумный ответ на подобный вопрос, одной программы недостаточно, необходима еще и ее спецификация, точно описывающая, что должна делать программа. Оператор
x:= y+1
сам по себе не является ни корректным, ни не корректным. Эти понятия приобретают смысл лишь по отношению к ожидаемому эффекту присваивания. Например, присваивание корректно по отношению к утверждению: "Переменные x и y имеют различные значения". Но не гарантируется его корректность по отношению к высказыванию: "переменная x отрицательна", поскольку результат присваивания зависит от значения y, которое может быть положительным.
Эти примеры иллюстрируют свойство, служащее отправной точкой в обсуждении проблемы корректности: программная система или ее элемент сами по себе ни корректны, ни не корректны. Корректность подразумевается лишь по отношению к некоторой спецификации. Строго говоря, мы и не будем обсуждать проблему корректности программных элементов, а лишь их согласованность (consistent) с заданной спецификацией. В наших обсуждениях мы будем продолжать использовать хорошо понимаемый термин "корректность", но всегда при этом помнить, что этот термин не применим к программному элементу, он имеет смысл лишь для пары - "программный элемент и его спецификация".
Свойство корректности ПО
Корректность - понятие относительное.
В этой лекции мы научимся выражать спецификации через утверждения (assertions), что поможет оценить корректность разработанного ПО.
Но пойдем дальше и перевернем проблему, - разработка спецификации является первым, важнейшим шагом на пути, гарантирующем, что ПО действительно соответствует спецификации. Существенную выгоду можно получить, когда спецификации пишутся одновременно с написанием программы, а лучше, до ее написания. Среди следствий такого подхода можно отметить следующее.
Разработка ПО корректного с самого начала, проектируемого так, чтобы быть корректным. Один из создателей структурного программирования Харлан Д. Миллс в семидесятые годы написал статью со знаменательным названием "Как писать корректные программы и знать это". Слово "знать" в данном контексте означает снабжать программу в момент ее написания аргументами, характеризующими корректность.Значительно лучшее понимание проблемы и достижение ее решения.Упрощение задачи создания программной документации. Как будет позже показано, утверждения будут играть важную роль в ОО-подходе к документации.Обеспечение основ для систематического тестирования и отладки.
Оставшаяся часть лекции посвящена исследованию этих вопросов. Одно предупреждение: языки программирования С, С++ и другие имеют оператор утверждения assert, динамически проверяющий истинность заданного утверждения в момент выполнения программы и останавливающий вычисление, если утверждение является ложным. Эта концепция, хотя и имеет отношение к предмету обсуждения, но является лишь малой частью использования утверждений в ОО-методе. Потому, если подобно многим разработчикам вы знакомы с этим оператором, не обобщайте ваше знание на всю картину, почти все концепции этой лекции, возможно, будут новыми.
Рассмотрим снова реализацию стека классом 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 дает суммарное значение списка всех операций (приходных или расходных). Инвариант определяет основное условие согласования всех банковских операций над счетом, связывая баланс, приходные и расходные операции.
Появление слова "жучок" в предыдущем анализе нарушений утверждений - хороший повод прояснить терминологию. Э. Дейкстра полагал, что появление термина "жучок" связано с жалкой попыткой программистов обвинить кого-то в том, что ошибка "закралась" в программу со стороны, пока программисты занимались делом, - как будто не разработчики повинны в ошибках. И все же термин прижился, возможно, из-за эмоциональной окраски и понятности. И в этой книге он свободно используется, но следует дополнить его более специфическими (и более нудными) терминами для случаев, когда необходима более строгая классификация ошибок.
Термины, обозначающие бедствия ПО
Ошибка (Error) - неверное решение, принятое при разработке программной системы.
Дефект (Defect) - свойство программной системы, которое может стать причиной отклонения системы от намеченного поведения.
Неисправность (Fault) - событие в программной системе, приведшее к отклонению от нормального поведения в процессе одного из запусков системы.
Причинные связи понятны: неисправности порождаются дефектами, являющиеся, в свою очередь, результатом ошибок.
"Жучок" обычно имеет смысл дефекта ("а вы уверены, что в вашей программе не осталось жучков"?). Такова его интерпретация в этой книге. Но в неформальных обсуждениях он может появляться и как ошибка и как неисправность.
Понятно ваше нетерпение и желание незамедлительно узнать, каков же эффект от утверждений при выполнении программы; что произойдет при вызове put при заполненном стеке, или что будет, когда empty дает true по завершении вызова put? Полный ответ на этот вопрос дать еще слишком рано, но предварительный использует любимое словечко адвокатов - это зависит (it depends).
Это зависит от того, что вы хотите. Можно рассматривать утверждения просто как комментарии, и тогда их нарушение не обнаруживается в период выполнения. Но их можно использовать для проверки того, что все идет по плану. Тогда во время выполнения окружение автоматически следит за выполнением утверждений и включает исключение при возникновении нарушений, завершая обычно выполнение и выводя сообщение об ошибке. Можно включить в программу обработку исключения, пытающуюся восстановить ситуацию и продолжить выполнение. Эта тема будет детально обсуждаться в следующей лекции. Для указания желаемой политики используются параметры компиляции, которые можно установить независимо для каждого класса.
Все детали мониторинга утверждений периода выполнения появятся чуть позже в этой лекции. Но было бы ошибкой на данном этапе уделять им много внимания. Другие аспекты утверждений сейчас важнее. Мы еще только приступили к рассмотрению этой техники, предназначенной, прежде всего, для создания корректного ПО; нам еще нужно многое открыть в их методологической роли встроенных стражей надежности. Вопрос о том, что случится, если возникнет ошибка, тоже важен, но рассматривать его следует после того, как мы сделаем все, чтобы предотвратить ее появление.
Посему, хотя и следует думать о будущем, не следует забивать себе голову вопросами о возможной потере производительности из-за введения конструкции old. Должна ли система сохранять значения перед запуском программы, чтобы иметь возможность вычислять old выражения? Это зависит: в некоторых обстоятельствах (например, при тестировании и отладке) полезно вычислять утверждения; в других - (для полностью проверенных систем) их можно рассматривать как аннотации программного текста.
Все это учитывается в следующих разделах, являясь методологическим вкладом утверждений и метода Проектирование по Контракту - концептуального средства анализа, проектирования, реализации и документирования, помогающего нам построить ПО со встроенной надежностью (reliability is built-in), в терминологии Миллса строить корректную программу и знать это.
Постусловие выражает свойство состояния, завершающего выполнение программы. Здесь:
После завершения put стек не может быть пуст; на его вершине находится только что втолкнутый элемент, число его элементов увеличилось на единицу.После remove стек не может быть полон, число его элементов на единицу уменьшилось.
Постусловие в программе выражает гарантию, представленную создателем программы, что выполнение программы завершается и приводит к состоянию с заданными свойствами, в предположении, что программа была запущена в состоянии, удовлетворяющем предусловию.
В постусловиях доступна специальная нотация old. Она используется, например, в программах remove и item для выражения изменения значения count. Запись old e, где e - выражение (в большинстве случаев - атрибут) обозначает значение, которое данное выражение имело на входе программы. Любое вхождение e, которому не предшествует old, означает значение выражения на выходе программы.
Постусловие программы put включает предложение:
count = old count + 1
устанавливающее, что put, примененное к любому объекту, должно увеличить на единицу значения поля count этого объекта.
Связывая с программой r предложения require pre и ensure post, класс говорит своим клиентам:
"Если вы обещаете вызвать r в состоянии, удовлетворяющем pre, то я обещаю в заключительном состоянии выполнить post".
В отношениях между людьми и компаниями контракт - это письменный документ, фиксирующий отношения. Удивительно, что в программной индустрии, где точность так важна и двусмысленность так рискованна, эта идея так долго не появлялась. Любой хороший контракт устанавливает для обоих участников как обязательства, так и приобретаемую выгоду; обычно обязательства одного оборачиваются выгодой для другого участника, и это взаимно. Все это верно и для контрактов между классами.
Предусловие связывает клиента: определяются условия, при которых вызов программы клиентом легитимен. Обязательства клиента приносят пользу поставщику.Постусловие связывает класс: программа обязана обеспечить условия по ее завершению. Здесь польза клиента оборачивается обязательствами поставщика класса.
Вот пример контракта для одной из программ нашего примера:
Клиент |
(Выполнить предусловие:) Вызывать put(x) только для непустого стека. |
(Из постусловия:) Получить обновленный стек: не пустой, x на вершине, (item дает x, count увеличилось на единицу). | ||
Поставщик |
(Выполнить постусловие:) Обновить представление стека: иметь x на вершине (item возвращает x), count увеличить на единицу, стек не пуст. |
(Из предусловия:) Упрощающее обработку предположение о том, что стек не пуст. |
Предусловия выражают ограничения, выполнение которых необходимо для корректной работы функции. Здесь:
put не может быть вызвана, если стек заполнен;remove и item не могут быть применены к пустому стеку.
Предусловия применяются ко всем вызовам программы, как внутри класса, так и у клиента. Корректная система никогда не вызовет программу в состоянии, в котором не выполняется ее предусловие.
Первое использование утверждений - семантическая спецификация программ. Программа - это не просто часть кода, она задает реализацию функции, входящей в спецификацию АТД. Задачу, выполняемую функцией, необходимо выразить точно, как в интересах проектирования, так и как цель последующей реализации и понимания программного текста. Два утверждения связываются с программой - предусловие и постусловие. Предусловие устанавливает свойства, которые должны выполняться всякий раз, когда программа вызывается; постусловие определяет свойства, гарантируемые программой по ее завершению.
Возможно, вы заметили необходимость дополнительного требования, не отраженного в принципе обоснованности предусловия. Для того чтобы клиент мог проверить предусловие, оно не должно использовать закрытые свойства класса, недоступность которых отражена в статусе экспорта.
Рассмотрим следующую ситуацию:
-- Предупреждение: это неправильный класс, только в целях иллюстрации. 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 является закрытым. Но ничего ошибочного в постусловии нет. Оно просто включает наряду со свойствами, полезными для клиентов ("Другие предложения"), свойство, имеющее смысл только для тех, кто знаком с полным текстом класса. Такие закрытые предложения не будут появляться в краткой форме класса - документации, предназначенной для авторов клиентских модулей.
Центральная идея Проектирования по контракту выражена в принципе Нет_Избыточности, суть которого в том, что за выполнение условия, необходимого для правильного функционирования программы, должен нести ответственность только один из партнеров контракта.
Какой же? В каждом случае есть две возможности.
Ответственность возлагается на клиента. В этом случае условие становится частью предусловия программы.За все отвечает поставщик. Тогда условие появится в программе, являясь частью разбора возможных ситуаций.
Первую ситуацию назовем требовательной (demanding), вторую - толерантной (tolerant). Класс STACK2 иллюстрирует требовательный стиль, толерантная версия, не содержащая предусловий, может выглядеть так:
remove is -- Удалить элемент вершины стека do if empty then print ("Ошибка: попытка удаления элемента из пустого стека") else count := count - 1 end end
Проводя аналогию с контрактами между людьми, требовательный стиль характерен для опытного поставщика, имеющего хорошо поставленное дело, и требующего от своих клиентов, чтобы они до обращения к нему выполнили всю необходимую предварительную работу. Толерантный стиль вызывает образ вновь образованной фирмы, старающейся завоевать своих клиентов, и выставляющей с этой целью рекламный плакат:
Какой же из стилей лучше? С первого взгляда может казаться, что толерантный стиль лучше, как с позиций повторного использования, так и для повышения надежности. В требовательном стиле на всех клиентов одного поставщика ложится ответственность за выполнение ряда условий; при повторном использовании число таких клиентов только возрастает. Так не эффективнее и надежнее было бы потребовать, чтобы эту ответственность брал на себя поставщик, освобождая клиентов от обязательств?
Исследуем эту проблему чуть глубже. Условие корректности описывает требования, необходимые для успешной работы программы. Толерантная версия программы remove является хорошим примером, демонстрирующим слабости этого стиля.
Действительно, что может сделать бедная, занимающаяся выталкиванием программа, когда стек пуст? Она делает храбрую попытку выдать явно неинформативное сообщение об ошибке, но на большее она не способна - ей недоступен контекст клиента, она не способна определить, что нужно делать, когда стек пуст. Только клиент - модуль, использующий стек для своих целей, например, модуль разбора текста в компиляторе, - обладает достаточной информацией для принятия нужного решения. Является ли это нормальным, хотя и бесполезным запросом, который следует просто проигнорировать. Если это ошибка, как следует ее обработать: выбросить ли исключение, попытаться скорректировать ситуацию, или, в крайнем случае, выдать информативное для пользователя сообщение об ошибке.
Обсуждая пример с квадратным корнем, приводился такой вариант программы:
if x < 0 then "Обработайте ошибку как-нибудь" else "Выполнить нормальное вычисление квадратного корня" end
Ключевое слово здесь "как-нибудь". Предложение then скорее заклинание, чем программный код: нет разумной, общецелевой техники обработки случая x<0. Только автор клиента может знать, что значит этот случай - ошибка в ПО, возможность замены нулевым значением, причина для возбуждения исключения...
Ситуация, в которую попала толерантная версия remove, напоминает почтальона, который должен доставить письмо, не содержащее ни адреса получателя, ни адреса отправителя, - немногое может сделать такой почтальон.
Соответствуя духу Проектирования по контракту, требовательный подход к проектированию предусловий не пытается создавать программы, выполняющие все для своих клиентов. Более того, его суть в том, что каждая программа выполняет только хорошо определенную часть работы, но делает ее хорошо (корректно, эффективно, способную повторно использоваться многими клиентами). Такая программа четко классифицирует случаи, с которыми она не может справиться. Автор программы не должен пытаться быть умнее своих клиентов, если он не уверен, что должна делать программа в некоторой критической ситуации, он должен исключить этот случай из программы и явно включить его в предусловие.
Эта позиция является следствием основной темы, проходящей через всю книгу, - создание программных систем как множества модулей, занятых своим делом.
Есть сходство в данном обсуждении и обсуждении использования частичных функций в математических моделях, рассматриваемое в лекции про АТД. Там говорилось, что целесообразнее использовать частичные функции, чем делать функцию всюду определенной, введением специального неопределенного значения - ?integer. Эти две идеи близки, Проектирование по контракту является частью применения к программным конструкциям концепции частичных функций, замечательно гибкого и мощного аппарата формальных спецификаций. |
Обычно следует избегать структур ограниченной емкости; даже в случае массивов можно строить стек на динамических массивах, изменяющих размерность при необходимости. В Базовой библиотеке представлен общий класс, описывающий стеки1), отличающийся от класса STACK2 тем, что в нем не используется понятие емкости; стек по умолчанию перестраивается, когда текущей емкости недостаточно для хранения очередного поступающего элемента. |
Давайте займемся дальнейшим исследованием предусловий и постусловий, рассматривая понятные элементарные примеры. Утверждения, некоторые простые, другие более детальные, будут проникать во все примеры в последующих лекциях.
Набросок библиотечного класса 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. Поскольку эффективная манипуляция с массивом требует доступа к системам низкого уровня, то эти программы будут реализованы с использованием внешних классов, что будет рассмотрено в последующих лекциях.
Свойство (2) правила инвариантов показывает, что неявно их можно рассматривать как добавления к предусловиям и постусловиям каждой экспортируемой программы класса. Посему принципиально понятие инварианта класса избыточно - это часть предусловий и постусловий программ.
Такое преобразование, конечно, не желательно. Это усложнило бы тексты программ, и, что более важно, - был бы утерян глубокий смысл инварианта, выходящий за пределы отдельных программ, применяемый к классу, как целому. Следует помнить, что инвариант применим не только к уже написанным программам класса, но и к тем, которые еще будут написаны. Он контролирует эволюцию класса, что будет отражено в правилах наследования.
Изменения в ПО неизбежны. Задача в том, чтобы уметь управлять ими. Этот подход соответствует принципам разработки, введенным в начале этой книги. Можно ожидать, что некоторые аспекты программных систем и их компонентов - классов - меняются чаще, чем другие. Добавление, удаление, изменение функциональности явление частое и нормальное. В этом изменчивом процессе все-таки хотелось бы иметь устойчивые свойства, в значительной степени, не подверженные изменениям. Именно эту роль играют инварианты, поскольку в них отражаются фундаментальные соотношения, характерные для класса. Конечно, в программных системах все может изменяться, едва ли можно гарантировать неприкосновенность любого из аспектов системы. Но фундамент остается фундаментом.
Класс STACK2 иллюстрирует базисные идеи, но оценить полную мощь инвариантов можно, лишь ознакомившись со всеми дальнейшими их примерами в остальной части этой книги. Понятие инварианта является одной из наиболее значимых концепций ОО-метода. Только после того, как я написал инвариант, (для разработанного мной класса), только после знакомства и понимания инвариантов (для изучаемого мной класса), только тогда я почувствовал, - я знаю, что такое класс.
Инвариант класса задает множество свойств объектов (экземпляров класса), которые должны выполняться в стабильные времена жизни объектов. В частности, эти свойства должны выполняться сразу после создания экземпляра объекта.
Стандартный механизм распределения инициализирует поля значениями по умолчанию соответствующих типов, приписанных атрибутам. Эти значения могут удовлетворять или не удовлетворять инварианту. Если нет, то требуется специальная процедура создания, инициализирующая значения атрибутов таким образом, чтобы инвариант выполнялся. Поэтому процедуру создания можно рассматривать, как операцию, гарантирующую, что все экземпляры класса начинают жить, имея корректный статус, - в котором инвариант выполняется.
При первом представлении процедур создания они рассматривались, как способ ответа на земной (и очевидный) вопрос, как переопределить инициализацию по умолчанию, если она не подходит для моего класса. Другая рассматриваемая проблема, - как задать несколько различных механизмов инициализации. Но теперь, с введением инвариантов и теоретического обсуждения, отраженного в правиле (1), мы видим более весомую роль процедур создания. Теперь они создают уверенность, что любой экземпляр класса, только начиная жить, удовлетворяет фундаментальным правилам своей касты - инварианту класса.
Разумное использование утверждений может помочь справиться с такими проблемами. Цикл может иметь связанное с ним утверждение, так называемый инвариант цикла (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 является максимумом массива, что и является требуемым результатом работы.
Понятия "сильнее" и "слабее" пришли из логики. Говорят, что P1 сильнее, чем P2, а P2 слабее, чем P1, если P1 влечет P2 и они не эквивалентны. Каждое утверждение влечет True, и из False следует все что угодно. Можно говорить, что True является слабейшим, а False сильнейшим из всех возможных утверждений.
Давайте взглянем на формулу корректности с позиций человека, собирающегося наняться на работу по выполнению операции А. Каковы с его точки зрения наилучшие предусловие P и постусловие Q, если у него есть возможность выбора? Возможность усиления предусловия означает, что можно предъявлять более жесткие требования к работодателю, что можно уменьшить число ситуаций, в которых следует приступать к выполнению работы. Так что сильное предусловие это "хорошие новости" для работника. Наилучшей для него работой - синекурой является работа, чья спецификация выражается формулой:
Синекура 1
{False} A {...}
Постусловие здесь не специфицировано, поскольку не имеет значения каково оно. К выполнению работы можно вообще не приступать, поскольку нет ни одного начального состояния, в котором предусловие было бы истинным. Так что если вам предложат такую синекуру, немедленно соглашайтесь, не глядя на постусловие - требования, предъявляемые к выполненной работе.
Именно такую спецификацию работ имел в виду начальник полиции одного из американских городов. Когда его спросили в интервью, почему он выбрал именно эту работу, он ответил: "Это единственная работа, где заказчик всегда неправ!" |
Для постусловия ситуация меняется на противоположную. Лучшими для работника являются более слабые условия - это "хорошие новости"; в этом случае хорошо нужно уметь делать очень немногое. Наилучшей работой - второй синекурой является работа, заданная спецификацией:
Синекура 2
{...} A {True}
Как бы не была выполнена работа, постусловие в этом случае будет истинным по определению. Кстати, почему эта работа является все-таки второй по предпочтительности? Причина, как можно видеть из определения триады Хоара, в завершаемости (terminate).
Определение устанавливает, что выполнение должно завершиться в состоянии, удовлетворяющем Q, всякий раз, когда оно начинается в состоянии, удовлетворяющем P. Для синекуры 1, где нет состояний, удовлетворяющих P, не имеет значения, что делает А даже если программный текст приводит к выполнению бесконечного цикла, или ломает компьютер. Любое А будет корректным по отношению к данной спецификации. Для синекуры 2, однако, требуется завершение работы, должно существовать заключительное состояние, не важно, что делает А, но то, что делается, должно быть выполнено за конечное время.
Читатели, знакомые с теорией, могли заметить, что формула {P} A {Q} определяет тотальную (total correctness) или полную корректность, включающую завершаемость наряду с соответствием спецификации. Свойство, устанавливающее, что программа удовлетворяет спецификации при условии ее завершения, известно, как частичная корректность. См. [M 1990] для детального знакомства с этими концепциями. |
Синтаксис цикла непосредственно следует из предшествующих соображений, определяющих ингредиенты цикла. Он будет включать элементы, отмеченные как необходимые.
Инвариант цикла inv - утверждение.Условие выхода exit, чья конъюнкция с inv дает желаемую цель.Вариант var - целочисленное выражение.Множество инструкций инициализации, которые всегда приводят к состоянию, в котором inv выполняется, а var становится неотрицательным.Множество инструкций body, которое (при условии, что оно начинается в состоянии, где var неотрицательно и выполняется inv), сохраняет инвариант и уменьшает var, в то же время следя за тем, чтобы оно не стало меньше нуля.Синтаксис цикла честно комбинирует эти ингредиенты:
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, следуя алгоритму Эвклида:
Класс, как неоднократно говорилось, является реализацией АТД, заданного формальной спецификацией или неявно подразумеваемого. В начале лекции отмечалось, что утверждения можно рассматривать, как способ введения в класс семантических свойств, лежащих в основе АТД. Давайте уточним наше понимание концепции утверждений, прояснив их связь с компонентами спецификации АТД.
(При первом чтении этот раздел можно опустить или ограничиться его беглым просмотром.)
Простые, но не защищенные модули могут быть не достаточно устойчивыми для использования их у произвольных клиентов. В таких случаях возникает необходимость создания нескольких классов, играющих роль фильтров. В отличие от ранее рассмотренных фильтров, устанавливаемых между внешним миром и обрабатывающими модулями, новые фильтры будут устанавливаться между "беспечными" клиентами с одной стороны и незащищенными классами с другой стороны.
Хотя было показано, что обычно это не лучший подход к проектированию, полезно рассмотреть, как выглядят классы, если использовать толерантный стиль в некоторых особых случаях. Класс 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
Толерантный подход остается полезным для модулей, принимающих данные от внешнего мира. Как отмечалось, в этом случае строятся фильтры, отделяющие внешний мир от обрабатывающих модулей. Класс STACK3 иллюстрирует идеи построения подобных фильтров. |
Возможность повторять некоторые вычисления произвольное число раз, не поддаваясь усталости, без случайных потерь чего-либо важного, - в этом принципиальное отличие компьютерных вычислений от возможностей человека. Вот почему циклы так важны. Трудно вообразить, что можно было бы делать в языках, в которых были бы только две управляющие структуры - последовательность и выбор, - но не было бы циклов и не было бы поддержки рекурсии, еще одного базисного механизма поддержки итеративных вычислений.
Но с мощностью приходят и риски. У циклов дурная слава, - их трудно заставить работать правильно. Типичными для циклов являются:
Ошибки "больше-меньше" (выполнение цикла слишком много или слишком мало раз).Ошибки управления пограничными ситуациями, например пустыми структурами. Цикл может правильно работать на больших массивах, но давать ошибки, когда у массива один элемент или он вообще пуст.Ошибки завершения ("зацикливание") в некоторых ситуациях.
Бинарный поиск - один из ключевых элементов базового курса "Введение в информатику" (Computer Science 101) - хорошая иллюстрация "коварства" циклов даже в относительно тривиальной ситуации. Рассмотрим целочисленный, упорядоченный по возрастанию массив t с индексами от 1 до n. Используем алгоритм бинарного поиска для ответа на вопрос: появляется ли целое x среди элементов массива. Если массив пуст, ответ должен быть "нет", если в массиве ровно один элемент, то ответ "да" тогда и только тогда, когда элемент массива совпадает с x. Суть бинарного поиска, использующего упорядоченность массива, проста: вначале x сравнивается со средним элементом массива, если есть совпадение, то задача решена, если x меньше среднего элемента, то поиск продолжается в верхней половине массива, в противном случае - в нижней половине. Каждое сравнение уменьшает размер массива вдвое. Ниже представлены четыре попытки реализации этой
простой идеи. К несчастью, все они содержат ошибки. Вам предоставляется случай поупражняться в поиске ошибок и установить, в какой ситуации каждый из алгоритмов не работает нужным образом.
Напомню, t @ m означает элемент массива t с индексом m. Знак операции // означает деление нацело, так что 7 // 2 и 6 // 2 дают значение 3. Синтаксис цикла будет дан ниже, но он должен быть и так понятен. Предложение from вводит инициализацию цикла. |
BS1 from i := 1; j := n until i = j loop m := (i + j) // 2 if t @ m <= x then i := m else j := m end end Result := (x = t @ i) | BS2 from i := 1; j := n; found := false until i = j and not found loop m := (i + j) // 2 if t @ m < x then i := m + 1 elseif t @ m = x then found := true else j := m - 1 end end Result := found |
BS3 from i := 0; j := n until i = j loop m := (i + j + 1) // 2 if t @ m <= x then i := m + 1 else j := m end end if i >= 1 and i <= n then Result := (x = t @ i) else Result := false end | BS4 from i := 0; j := n + 1 until i = j loop m := (i + j) // 2 if t @ m <= x then i := m + 1 else j := m end end if i >= 1 and i <= n then Result := (x = t @ i) else Result := false end |
Напишите спецификацию АТД для класса COMPLEX, описывающую понятие комплексных чисел с арифметическими операциями. Исходите из точной арифметики.
Напишите класс, реализующий очередь (стратегию доступа "первый пришел - первый ушел", FIFO - "first in - first out"). Задайте подходящие утверждения в стиле класса STACK этой лекции.
Проверьте все предусловия и аксиомы АТД STACK, введенного в предыдущих лекциях, и покажите, отображаются ли они в классе STACK4, а если да, то как.
Покажите, что введение закрытой функции body, возвращающей тело стека, сделает возможным утверждениям класса STACK полностью отражать спецификацию соответствующего АТД. Обсудите теоретическую и практическую значимость такого подхода.
Почему capacity экспортируется для реализации стеков ограниченных размеров, класс STACK2?
Обсудите использование функций в утверждениях, в частности, введение функции correct_index в предусловия программ put и item. Если добавить эту функцию в класс ARRAY, то какой статус экспорта следует ей дать?
Покажите, что каждая из четырех попыток бинарного поиска, объявленная как "ошибочная", действительно некорректна. (Подсказка: в отличие от доказательства корректности, для доказательства некорректности достаточно предъявить один пример, на котором алгоритм приводит к неверному результату: не завершается, выполняет запрещенную операцию, такую, как выход индекса за допустимые границы, любое другое нарушение предусловия).
В этой лекции было показано, что нарушение предусловия указывает на ошибку клиента, а нарушение постусловия указывает на ошибку поставщика. Объясните, почему нарушение инварианта также указывает на ошибку поставщика.
Напишите класс, реализующий алгоритм получения псевдослучайных чисел, основанный на последовательности: ni = f(ni - 1), где функция f задана, а начальное значение n0 определяется клиентом класса. Функция не должна иметь побочных эффектов. Определение функции f можно найти в учебниках, таких как [Knuth 1981] и в библиотеках по численным методам.
Напишите класс, реализующий множество элементов произвольного типа со стандартными операциями: проверка принадлежности, добавление нового элемента, объединение, пересечение и другими. Не забудьте включить подходящие утверждения. Приемлема любая корректная реализация, основанная на массивах или связных списках.
Еще одно типичное заблуждение - рассматривать утверждения как управляющую структуру, реализующую разбор случаев. К этому моменту должно быть ясно, что не в этом их роль. Если написать программу sqrt, в которой отрицательные значения будут обрабатываться одним способом, а положительные - другим, то писать предусловие - предложение require не следует. В этом случае используется обычный разбор случаев: оператор if - then - else, или оператор case языка Pascal, или оператор inspect, введенный в этой книге как раз для таких целей.
Утверждения выражают нечто иное. Они говорят о корректности условий. Если sqrt имеет предусловие, то вызов, в котором x<0, это "жучок" (bug).
Правило нарушения утверждения (1)
Нарушение утверждения в период выполнения является проявлением "жучка" в ПО.
Слово "жучок" не принадлежит к научному лексикону, но этот термин понятен всем программистам. Учитывая контракты, это правило можно уточнить:
Правило нарушения утверждения (2)
Нарушение предусловия является проявлением "жучка" у клиента.
Нарушение постусловия является проявлением "жучка" у поставщика.
Нарушение предусловия означает, что вызывающая программа нарушила контракт - "виноват заказчик". С позиций внешнего наблюдателя можно, конечно, критиковать сам контракт, но коль скоро контракт заключен, его следует выполнять. Если есть программа, осуществляющая мониторинг утверждений, то запускать на выполнение программу, чье предусловие не выполняется, не имеет смысла.
Нарушение постусловия означает, что программа, предположительно вызванная в корректных условиях, не выполнила свою часть работы, предусмотренную контрактом. Здесь тоже ясно, кто виноват, а кто нет: "жучок" в программе, клиент не виновен.
Первое использование является чисто методологическим и, вероятно, самым важным. В деталях оно рассматривалось в предыдущих разделах: точные требования к каждой программе, глобальные свойства классов и циклов - все это помогает разработчикам производить программный продукт, корректный с самого начала в противоположность подходу, пытающемуся добиться корректности в процессе отладки. Преимущества точной спецификации и систематического подхода к конструированию программ не могут быть преувеличены. Во всей этой книге всякий раз при встрече с программным элементом его формальные свойства выражались точно, насколько это было возможным.
Ключевая идея этой лекции - Проектирование по контракту. Использование компонент некоторого модуля является контрактом с его службами. Хорошие контракты точно специфицируют и ограничивают права и обязанности каждого участника. В проектировании ПО, где корректность и устойчивость так важны, необходимо раскрытие терминов контракта, как предварительное условие их следованию. Утверждения дают способ точно установить, что ожидается и что гарантируется каждой стороне в этом соглашении.
Полезно сосредоточиться на некоторых неявно обсуждавшихся свойствах контрактов. Заметьте, контракты описывают только взаимодействие двух программ (программа - программа). Контракты не задают другие виды взаимодействий: человек - программа, внешний мир - программа. Предусловие не заботится о корректировке ввода пользователя, например программа read_positive_integer, ожидающая в интерактивном режиме ввода пользователем положительного целого. Включение в такую программу предусловия:
require input > 0
хотя и желательно, но технически не реализуемо. Полагаться на пользователя в контрактах нельзя. В данной ситуации нет заменителя обычной конструкции проверки условия, включая почтенный if - then - else; полезен и механизм обработки исключений.
У утверждений своя роль в решении проблемы проверки ввода данных. При описании критерия Защищенности модуля отмечалось, что Метод поощряет проверку правильности любых объектов, получаемых из внешнего мира - от сенсоров, пользовательского ввода, из сети и т. д. Эта проверка должна быть максимально приближена к источникам объектов, используя при необходимости модули - "фильтры".
При получении информации извне нельзя опираться на предусловия. Задача модулей ввода - гарантировать, что никакая информация не будет передана обрабатывающим модулям, пока она не будет удовлетворять условиям, требуемым для корректной обработки. При таком подходе утверждения будут широко использоваться в коммуникациях программа - программа. Постусловия модулей ввода должны соответствовать или превосходить предусловия, продиктованные обрабатывающими модулями. Фильтры играют охраняющую роль, обеспечивая корректность входных данных.
Булевы выражения не ограничиваются использованием атрибутов и локальных сущностей. Мы уже использовали возможность вызова функций в утверждениях: предусловие для 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 дает максимальный элемент этого массива.
Этот подход был исследован в [M 1995a] как способ расширения выразительной силы механизма утверждений, возможно ведущий к разработке полностью формального метода, - другими словами, к математическому доказательству корректности ПО. В этом исследовании есть две центральные идеи. Первая - использование библиотек в процессе доказательства, так что можно его проводить для реальных, широкомасштабных систем, строя многоярусную структуру, использующую условные доказательства. Вторая идея - определение ограниченного языка чисто аппликативной природы - IFL (Intermediate Functional Language), в котором выражаются функции, используемые в выражениях. Язык IFL является подмножеством нотации этой книги, включающий некоторые императивные конструкции, такие как любые присваивания. |
Как только корректность ПО определена как согласованность реализации с ее спецификацией, следует предпринять шаги по включению спецификации в сам программный продукт. Для большинства в программистском сообществе это все еще новая идея. Привычно писать программы, устанавливая тем самым, - как делать (the how); менее привычно рассматривать описание целей - что делать (the what) - как часть программного продукта.
Спецификации будут основываться на утверждениях - выражениях, включающих сущности нашего ПО. Выражение задает свойство, которому эти сущности могут удовлетворять на некоторых этапах выполнения программы. Типичное утверждение может выражать тот факт, что определенное целое имеет положительное значение, или что некоторая ссылка не определена.
Ближайшим к утверждению математическим понятием является предикат, хотя используемый язык утверждений обладает лишь частью выразительной силы полного исчисления предикатов.
Синтаксически утверждения в нашей нотации будут обычными булевыми выражениями с небольшими расширениями. Одним из расширений является введение в нотацию термина "old", другим - введение символа ";" для обозначения конъюнкции (логического И). Вот пример:
n>0; x /= Void
Как между объявлениями и операторами, стоящими на разных строках, символ ";" является возможным, но не обязательным, так и в последовательности утверждений, записанных на разных строках, он может быть опущен, подразумеваясь по умолчанию. Эти соглашения облегчают идентификацию индивидуальных компонентов утверждения, которым обычно даются имена:
Positive: n > 0 Not_void: x /= Void
Метки, такие как Positive и Not_Void, в период выполнения играют роль утверждений, что будет еще обсуждаться в этой лекции. В данный момент они введены, главным образом, для ясности и документирования. В нескольких последующих разделах будет дан обзор принципиальных возможностей применения утверждений: как концептуального средства, позволяющего создавать корректные системы, и как документирование того, почему они корректны.
Из соответствия между АТД функциями и компонентами класса можно вывести соответствие между утверждениями класса и семантическими свойствами АТД.
Предусловие для специфицированной в АТД функции появляется как предусловие программы, соответствующей данной функции.Аксиома, включающая команду, и, возможно, одну или более функций запросов, появится как постусловие соответствующей процедуры.Аксиомы, включающие только запросы, появятся как постусловия соответствующих функций или как инвариант. Последнее обычно имеет место, если более чем одна функция включена в аксиому, или, по меньшей мере, один из запросов реализован в виде атрибута.Аксиомы, включающие функцию создатель, появятся в постусловии соответствующей процедуры создания.
В этот момент следует вернуться назад и сравнить аксиомы АТД STACK с утверждениями класса STACK4 (включая и те, которые даны для класса STACK2).
От неформальных высказываний перейдем к простой математической нотации, принятой в теории формальной проверки правильности программ и имеющей ценность при доказательстве корректности программных элементов.
Как можно было заметить, применяемый язык утверждений является языком обычных булевых выражений, обогащенный несколькими понятиями, такими как 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.
Вместо этого, в механизме утверждений мы пошли на инженерный компромисс: он включает достаточно формальных элементов, оказывающих существенный эффект на качество ПО, но останавливается в точке убывания - границе, за которой выгоды от большей формализации, начинают оборачиваться потерями простоты и эффективности.
Определение границы во многом определяется личным выбором. Я был удивлен, для программистского сообщества в целом эта граница не изменилась со времен первого издания этой книги. Наша деятельность требует большего формализма, но профессиональное сообщество еще не осознало этого. |
Предусловие в процедуре создания (конструкторе) make класса STACK1 требует комментария. Оно устанавливает n>=0 и, следовательно, допускает пустые стеки. Если n=0, то make вызовет процедуру создания для массивов, также имеющую имя make, с аргументами 1 и 0 для нижней и верхней границ соответственно. Это не ошибка, это соответствует спецификации процедуры создания массивов, которая в случае, когда нижняя граница на единицу больше верхней, создает пустой массив.
Пустой стек не ошибка, это особый случай. Ошибка может возникнуть при попытке чтения из пустого стека, но этот случай охраняется предусловиями put и item.
При определении общих структур данных, подобных стеку или массиву, возникает вопрос о концептуальной целесообразности пустой структуры. В зависимости от ситуации ответ может быть разный, например, для деревьев полагается обычно, что дерево должно иметь хотя бы один узел - корень. Но в случае стеков или массивов, когда нет логической невозможности существования пустой структуры, ее следует допускать.