Relations

RequirementsEnsureInvariants

Requirements

Limits the domain of the used variables by adding relations which must be satisfied before the code block can be entered.

Ensure

Guarantees a domain limitation of the used variable after the code block has exited; however, this is not guaranteed when the code block fails.

Invariants

Declares a relation to be always true during the code block even if the code block fails.