Descriptions A class invariant denotes a formula that is implicitly added
As an exception, if the constructor or object method is marked as a , then the formula is added neither to the precondition nor to the postcondition.
Pragmatics A class invariant ensures that, after the allocation of an object, during its full life-time, at every call/return from a (non-helper) method invoked on that object, the stated formula holds.