Бертран Мейер - Основы объектно-ориентированного программирования

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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