Ключевые концепции. Еще не все сделано с Проектированием по контракту

Что дальше

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Дата добавления: 2014-01-07