Инварианты и контракты

Инварианты и контракты

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

Давайте пойдем дальше. Выше отмечалось, что инварианты можно рассматривать как добавки к предусловиям и постусловиям экспортируемых программ. Пусть body тело программы, pre - предусловие, post - постусловие, Inv - инвариант программы. Требование корректности программы может быть записано в виде:

{INV and pre} body {INV and post}

Это означает, что любое выполнение body, начинающееся в состоянии, удовлетворяющем Inv и pre, завершится в состоянии, в котором выполняются Inv и post. Для человека, создающего body, появление инварианта является "хорошей" или "плохой" новостью, облегчается или затрудняется его задача? Ответ, как следует из предыдущих обсуждений, и да и нет! Вспомним ленивого работника, который мечтает о сильном предусловии и слабом постусловии, чтобы можно было бы работать как можно меньше. Инвариант усиливает как предусловие, так и постусловие. Так что, если вы ответственны за реализацию body, то добавление инварианта:

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

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

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

Класс BANK_ACCOUNT, упоминавшийся выше, с инвариантом класса:

deposits_list.total - withdrawals_list.total = balance

дает хороший пример. При добавлении в класс новой программы гарантируется, что свойства deposits_list, withdrawals_list, balance имеют согласованные значения, посему нет необходимости в проверках согласованности. Но это также означает, что при написании программы следует следить за сохранением согласованности. Так что процедура withdraw, которая занимается снятием некоторых сумм со счетов, должна в конце работы изменить соответственно и баланс - атрибут balance.

Заметьте, balance может быть не атрибутом, а функцией, возвращающей значение, вычисляемое, например, так: deposits_list.total - withdrawal_list.total. В этом случае процедуре withdraw вообще ничего не нужно делать для обеспечения выполнимости инварианта. Возможность переключаться между двумя представлениями (атрибута и функции) без влияния на клиента обеспечивается принципом Унифицированного доступа.
Поделитесь на страничке

Следующая глава >

Похожие главы из других книг:

Контракты и надежность ПО

Из книги автора

Контракты и надежность ПО Предусловие и постусловие программы определяют контракт со всеми ее


Инварианты класса

Из книги автора

Инварианты класса Предусловия и постусловия описывают свойства отдельных программ. Но экземпляры класса обладают также глобальными свойствами. Их принято называть инвариантами класса (class invariants), и они определяют более глубокие семантические свойства и ограничения


Инварианты реализации

Из книги автора

Инварианты реализации Некоторые утверждения появляются в реализации, хотя они не имеют прямых двойников в спецификации АТД. Эти утверждения используют атрибуты, включая некоторые закрытые атрибуты, которые, по определению, не имеют смысла в АТД. Простым примером


Инварианты и варианты цикла

Из книги автора

Инварианты и варианты цикла Наши следующие и последние конструкции утверждений помогут строить корректные циклы. Эти конструкции являются прекрасным дополнением рассмотренных ранее механизмов. Поскольку они не являются специфической частью ОО-метода, то вы вправе


Инварианты класса и семантика ссылок

Из книги автора

Инварианты класса и семантика ссылок ОО-модель, разрабатываемая до сих пор, включала два частично не связанных аспекта, оба из которых полезны:[x]. Понятие инварианта класса, введенное в этой лекции.[x]. Гибкая модель периода выполнения, детально рассмотренная в начальных


Инварианты

Из книги автора

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


Как мы планируем релизы и составляем контракты с фиксированной стоимостью

Из книги автора

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