5.6. Contract modes: free and checked
Every plain contract clause has two sides: it is asserted at one end and assumed at the
other. A requires is proved by the caller and assumed by the body; an ensures is proved by the
body and assumed by the caller. The free and checked modifiers keep only one of those sides.
Clause | Asserted | Assumed |
|---|---|---|
| yes, at every call site | yes, in the body |
| no | yes, in the body |
| yes, at every call site | no |
| yes, at every exit of the body | yes, after every call |
| no | yes, after every call |
| yes, at every exit of the body | no |
So free is trusted information: it is believed without proof, and it is the right tool for an
assumption that comes from outside the program — a fact about a boundary the analysis cannot see.
Because nothing checks it, a wrong free clause can make the analysis prove things the program
does not satisfy; treat each one as an axiom you are adding.
checked is the opposite: the property is proved but deliberately not handed to the other side.
It is useful for a property you want enforced without letting callers depend on it, so that it
stays free to change.
procedure boundaryRead(handle: int) returns (r: int) free requires handle > 0 opaque ensures r >= 0 checked ensures r != 42;