cprover
|
Back to Code Contracts User Documentation
A requires clause specifies a precondition for a function, i.e., a property that must hold to properly execute the function. Developers may see the requires clauses of a function as obligations on the caller when invoking the function. The precondition of a function is the conjunction of the requires clauses, or true if none are specified.
An ensures clause specifies a postcondition for a function, i.e., a property over arguments or global variables that the function guarantees at the end of the operation. Developers may see the ensures clauses of a function as the obligations of that function to the caller. The postcondition of a function is the conjunction of the ensures clauses, or true if none are specified.
Both requires clauses and ensures clauses take a Boolean expression over the arguments of a function and/or global variables. The expression can include calls to CBMC built-in functions, to Memory Predicates or to function pointer predicates. User-defined functions can also be called inside requires clauses as long as they are deterministic and do not have any side-effects (the absence of side effects is checked by the tool). In addition, ensures clauses also accept History Variables and the special built-in symbol __CPROVER_return_value which represents the return value of the function.
The semantics of ensures and requires clauses can be understood in two contexts: enforcement and replacement. To illustrate these two perspectives, consider the following implementation of the sum function.
In order to determine whether requires and ensures clauses are a sound abstraction of the behavior of a function f, CBMC will try to check them as follows:
In our example, the sum function will be instrumented as follows:
Assuming requires and ensures clauses are a sound abstraction of the behavior of the function f, CBMC will use the function contract in place of the function implementation as follows:
In our example, consider that a function foo may call sum.
CBMC will use the function contract in place of the function implementation wherever the function is called.