Language features: Contracts

code

Syntax

 

New attributes: expects, ensures, assert – contract tools

The following attributes specifies preconditions, postconditions, and assertions for functions.

All of the predicates must be convertible to bool for interrogation purposes.

They are both documentation and runtime asserts of how the caller should be expected to call the functions and in what state can the caller expect the code to be after the function has returned.

 

In case the precondition fails, further execution is not guaranteed – either the program aborts, or throws an exception, or if it is allowed to continue then the behavior is undefined. Whichever of these alternatives is chosen is implementation-defined.

In case the postcondition fails, the program is abnormally terminated as in the pre-condition case. The postcondition of a function is not evaluated as part of an exceptional transfer of control.

Full Syntax

  • contract-attribute: expects, ensures, and assert
  • conditional-expression: the predicate of the contract
  • modifier: specifies the contract level or the enforcement of the contract – default, audit, and axiom
    • off: no contract checking is performed.
    • default (default if no build level is selected): checking is performed for contracts whose contract-level is default.
    • audit: checking is performed for contracts whose contract-level is default or audit.

Leave a comment

Your email address will not be published.