Инварианты
Инварианты
С правилом об инвариантах класса мы встречались и прежде:
Правило родительских инвариантов
Инварианты всех родителей применимы и к самому классу.
Инварианты родителей добавляются к классу. Инварианты соединяются логической операцией and then. (Если у класса нет явного инварианта, то инвариант True играет эту роль.) По индукции в классе действуют инварианты всех его предков, как прямых, так и косвенных.
Как следствие, выписывать инварианты родителей в инварианте потомка еще раз не нужно (хотя семантически такая избыточность не вредит: a and then a есть то же самое, что a).
Полностью восстановленный инвариант класса можно найти в плоской и краткой плоской форме последнего (см. лекцию 15).
Более 800 000 книг и аудиокниг! 📚
Получи 2 месяца Литрес Подписки в подарок и наслаждайся неограниченным чтением
ПОЛУЧИТЬ ПОДАРОКЧитайте также
Инварианты класса
Инварианты класса Предусловия и постусловия описывают свойства отдельных программ. Но экземпляры класса обладают также глобальными свойствами. Их принято называть инвариантами класса (class invariants), и они определяют более глубокие семантические свойства и ограничения
Инварианты и контракты
Инварианты и контракты В метафоре контрактов интерпретация инвариантов ясна и понятна. В сообществе людей все контракты часто содержат ссылки на общие правила, регулирующие отношения между партнерами независимо от конкретной области применения контракта. Например
Инварианты реализации
Инварианты реализации Некоторые утверждения появляются в реализации, хотя они не имеют прямых двойников в спецификации АТД. Эти утверждения используют атрибуты, включая некоторые закрытые атрибуты, которые, по определению, не имеют смысла в АТД. Простым примером
Инварианты и варианты цикла
Инварианты и варианты цикла Наши следующие и последние конструкции утверждений помогут строить корректные циклы. Эти конструкции являются прекрасным дополнением рассмотренных ранее механизмов. Поскольку они не являются специфической частью ОО-метода, то вы вправе
Инварианты класса и семантика ссылок
Инварианты класса и семантика ссылок ОО-модель, разрабатываемая до сих пор, включала два частично не связанных аспекта, оба из которых полезны:[x]. Понятие инварианта класса, введенное в этой лекции.[x]. Гибкая модель периода выполнения, детально рассмотренная в начальных