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

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

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] представляет обзор этого направления.