Keyword: assert

A statement that guarantees that a given proposition is true.

Assertions are checked statically as part of checking an action. They are considered an internal part of the action's body rather than precondition and postcondition contracts that are made visible to the caller of the action.

The exact relationship between assertions, assumptions, preconditions and postconditions is discussed on the weakest liberal precondition page, and the page on assume-guarantee reasoning.