Invariants

An invariant is a logical expression that must always hold true. They can be used to validate state changes in entities, or parameter values in functions.

• Entities - specifies a rule on the state of an entity
• Functions - specifies a rule on the input parameters of a function

Nothing