Class invariants are conditions that have to be met by any stable state of an object. Stable states exists before and after every execution of an interface routine from the outside of an object. (Note that when an interface routine is called locally from within an object, it does not have to be in a stable state.)
BNF:
class-decl ::= class identifier [ "<" generics-list ">"] is
class-definition
class-definition ::= ...
| [ identifier ] general-class-decl
general-class-decl ::= ...
[ invariant condition ]
end class
Invariants are checked at runtime before and after every external interface routine call and after execution of the creation routine. A runtime error is generated if an invariant evaluates to false.