cprover
|
Back to Code Contracts User Documentation
CBMC offers support for loop contracts, which includes four basic clauses:
These clauses formally describe an abstraction of a loop for the purpose of a proof. CBMC also provides a series of built-in constructs to aid writing loop contracts (e.g., history variables and quantifiers).
Consider an implementation of the binary search algorithm below.
The function stores a lower bound lb
and an upper bound ub
initialized to the bounds on the buffer buf
, i.e., to 0
and size-1
respectively. In each iteration, the midpoint mid
is compared against the target value val
and in case of a mismatch either the lower half or the upper half of the buffer is searched recursively. A developer might be interested in verifying two high-level properties on the loop on all possible buffers buf
and values val
:
buf[mid]
lookup)To prove the first (memory-safety) property, we may declare a _loop invariant_ that must be preserved across all loop iterations. In this case, two invariant clauses would together imply that buf[mid]
lookup is always safe. The first invariant clause would establish that the bounds (lb
and ub
) are always valid:
Note that in the second conjunct, the lb - 1 == ub
case is possible when the value val
is not found in the buffer buf
. The second invariant clause would establish that the midpoint mid
is always a valid index. In this particular case we can in fact establish a stronger invariant, that mid
is indeed always the midpoint of lb
and ub
in every iteration:
To prove the second (termination) property, we may declare a _decreases clause_ that indicates a bounded numeric measure which must monotonically decrease with each loop iteration. In this case, it is easy to see that lb
and ub
are approaching closer together with each iteration, since either lb
must increase or ub
must decrease in each iteration.
The loop together with all its contracts is shown below.
With CBMC we can now generate an unbounded proof using these contracts:
The first command compiles the program to a GOTO binary, next we instrument the loops using the annotated loop contracts, and finally we verify the instrumented GOTO binary with desired checks.