The following assertion types are part of PbC:
Pre-condition: An assertion checked before a function/method body is executed.
Post-condition: An assertion checked before a function/method exits, including exception control flow.
Loop invariant: An assertion that is true at the beginning of the loop and after each execution of the loop body.
Loop variant: An assertion that describes how the data in the loop condition is changed by the loop. It is used to check forward progress in the execution of loops to avoid infinite loops and other incorrect loop behavior.
Loop bounds: An assertion that checks that the loop can only be traversed a bounded number of times.
Class invariant: An assertion that is evaluated before and after each invocation of a public function and can be thought of as a way to factorize contracts.
Assertion: An assertion not attached to standard language constructs.
The main purpose of contracts is to clearly define responsibilities between the supplier (the callee must fulfill post-conditions) and the consumer (the caller must fulfill pre-conditions), and hence help to avoid errors that are caused by ambiguity. Compliance is tested with executable code that can be optionally compiled into the application.