Requirements | Ensure | Invariants |
Limits the domain of the used variables by adding relations which must be satisfied before the code block can be entered.
Guarantees a domain limitation of the used variable after the code block has exited; however, this is not guaranteed when the code block fails.
Declares a relation to be always true during the code block even if the code block fails.