9 Declarations [dcl.dcl]

9.11 Attributes [dcl.attr]

9.11.4 Contract attributes [dcl.attr.contract]

9.11.4.1 Syntax [dcl.attr.contract.syn]

1
#
Contract attributes are used to specify preconditions, postconditions, and assertions for functions.
contract-attribute-specifier:
	[ [ expects contract-level : conditional-expression ] ]
	[ [ ensures contract-level identifier : conditional-expression ] ]
	[ [ assert contract-level : conditional-expression ] ]

contract-level:
	default
	audit
	axiom
An ambiguity between a contract-level and an identifier is resolved in favor of contract-level.
2
#
It expresses a function's expectation on its arguments and/or the state of other objects using a predicate that is intended to hold upon entry into the function.
The attribute may be applied to the function type of a function declaration.
3
#
It expresses a condition that a function should ensure for the return value and/or the state of objects using a predicate that is intended to hold upon exit from the function.
The attribute may be applied to the function type of a function declaration.
A postcondition may introduce an identifier to represent the glvalue result or the prvalue result object of the function.
[ Example
: 
int f(char * c)
  [[ensures res: res > 0 && c != nullptr]];

int g(double * p)
  [[ensures audit res: res != 0 && p != nullptr && *p <= 0.0]];
— end example
 ]
4
#
It expresses a condition that is intended to be satisfied where it appears in a function body.
The attribute may be applied to a null statement ([stmt.expr]).
An assertion is checked by evaluating its predicate as part of the evaluation of the null statement it applies to.
5
#
Preconditions, postconditions, and assertions are collectively called contracts.
The conditional-expression in a contract is contextually converted to bool ([conv]); the converted expression is called the predicate of the contract.
[ Note
:
The predicate of a contract is potentially evaluated ([basic.def.odr]).
— end note
 ]
6
#
The only side effects of a predicate that are allowed in a contract-attribute-specifier are modifications of non-volatile objects whose lifetime began and ended within the evaluation of the predicate.
An evaluation of a predicate that exits via an exception invokes the function std​::​terminate ([except.terminate]).
The behavior of any other side effect is undefined.
[ Example
: 
void push(int x, queue & q)
  [[expects: !q.full()]]
  [[ensures: !q.empty()]]
{
  /* ... */
  [[assert: q.is_valid()]];
  /* ... */
}

int min = -42;
constexpr int max = 42;

constexpr int g(int x)
  [[expects: min <= x]]                         // error
  [[expects: x < max]]                          // OK
{
  /* ... */
  [[assert: 2*x < max]];
  [[assert: ++min > 0]];                        // undefined behavior
  /* ... */
}
— end example
 ]