Книга: Основы объектно-ориентированного программирования
Ключевые концепции
Ключевые концепции
[x]. Утверждения - это булевы выражения, задающие семантические свойства класса и вводящие аксиомы и предусловия соответствующего абстрактного типа данных.
[x]. Утверждения используются в предусловиях (требования, при выполнении которых программы применимы), постусловиях (свойства, гарантируемые на выходе программ), и инвариантах класса (свойства, характеризующие экземпляры класса во время их жизни). Другими конструкциями, включающими утверждения, являются инварианты цикла и инструкции check.
[x]. Предусловие и постусловие программы описывают контракт между программой и ее клиентами. Контракт связывает программу, только при условии ее вызова, в состоянии, где предусловие выполняется; в этом случае программа гарантирует выполнимость постусловия на выходе. Понятие заключения контрактов между программами обеспечивает мощную метафору при построении надежного ПО.
[x]. Инвариант класса выражает семантические ограничения экземпляров класса. Инвариант неявно добавляется к предусловиям и постусловиям каждой экспортируемой программы класса.
[x]. Класс описывает одну возможную реализацию АТД; отображение класса в АТД выражается функцией абстракции, обычно частичной. Обратное отношение, обычно, не задается функцией.
[x]. Инвариант реализации, - часть инварианта класса - выражает корректность представления классом соответствующего АТД.
[x]. Цикл может иметь инвариант цикла, позволяющий вывести результат выполнения цикла, и вариант, позволяющий доказать завершаемость цикла.
[x]. Если класс поставляется с утверждениями, то можно формально определить, что означает корректность класса.
[x]. Утверждения служат четырем целям: помогают в конструировании корректных программ; помогают в создании документации, помогают в отладке, являются основой механизма исключений.
[x]. Язык утверждений в нашей нотации не включает логику предикатов первого порядка, но может выражать многие свойства высокого уровня благодаря вызову функций. Функции, включаемые в утверждения должны быть простыми и безупречно корректными.
[x]. Комбинация инвариантов и динамических псевдонимов приводит к Непрямому Эффекту Инварианта, который может стать причиной нарушения инварианта при корректности самого класса.
- Базисные механизмы надежности
- О корректности ПО
- Выражение спецификаций
- Введение утверждений в программные тексты
- Предусловия и постусловия
- Контракты и надежность ПО
- Работа с утверждениями
- Инварианты класса
- Когда класс корректен?
- Связывание с АТД
- Инструкция утверждения
- Инварианты и варианты цикла
- Использование утверждений
- Обсуждение
- Ключевые концепции
- Библиографические замечания
- Упражнения
- Постскриптум: Катастрофа Ариан 5