Использование утверждений
Предусловие связывает клиента, постусловие - поставщика.
Делайте предусловие достаточно сильным, чтобы программа могла хорошо делать свою работу, - но не сильнее.
Два вида предложений инварианта: некоторые предложения идут от лежащей в основе абстракции данных, другие (инвариант представления) описывают согласованные свойства реализации. Используйте инвариант, чтобы выразить и улучшить ваше понимание отношений между различными составляющими класса, в частности атрибутами.
Для запросов без аргументов включайте абстрактные свойства в инвариант (даже если для функции свойство появляется в виде постусловия).
При повторном объявлении допустимо ослабление предусловий, позволяющее расширить область применения подпрограммы.
Для достижения эффекта усиления предусловия используйте абстрактные предусловия (основанные на булевых функциях) в оригинале.
Даже и без необходимости усиления абстрактные предусловия являются предпочтительными.
Любое предусловие должно обеспечиваться и проверяться клиентом перед вызовом компонента.
Не усердствуйте в усилении постусловий - оставьте возможность их усиления потомками (например, можно оставить одностороннюю импликацию implies вместо эквивалентности).