A specifier for contracts that must be satisfied before the function is ran.

Specifiers

pre(predicate)
post(predicate)

Example

int divide(int dividend, int divisor) pre(divisor != 0)
{
    return dividend / divisor;
}
 
double square_root(double num) pre(num >= 0)
{
    return std::sqrt(num);
}
 
int absolute_value(int num) post(r : r >= 0)
{
    return std::abs(num);
}