Инварианты

Инварианты

С правилом об инвариантах класса мы встречались и прежде:

Правило родительских инвариантов

Инварианты всех родителей применимы и к самому классу.

Инварианты родителей добавляются к классу. Инварианты соединяются логической операцией and then. (Если у класса нет явного инварианта, то инвариант True играет эту роль.) По индукции в классе действуют инварианты всех его предков, как прямых, так и косвенных.

Как следствие, выписывать инварианты родителей в инварианте потомка еще раз не нужно (хотя семантически такая избыточность не вредит: a and then a есть то же самое, что a).

Полностью восстановленный инвариант класса можно найти в плоской и краткой плоской форме последнего (см. лекцию 15).