4.2. Postconditions and opaque procedures🔗

Laurel allows a procedure to be marked as opaque, which means that callers won't be able to reason about the body of the procedure. Once a procedure is opaque, Laurel allows defining postconditions for it, which remain visible to the caller. Postconditions allow encapsulating the body of a procedure using simpler conditions, making it easier to reason about by callers.

Laurel does not allow postconditions on procedures with transparent bodies, because a postcondition can only contain information that can also be inferred from the body, and redundant information is bad for verification performance.

For proving properties on top of a procedure's body or postconditions, define a separate procedure that calls the target one. Such a separate 'lemma' procedure can be invoked automatically using an invokeOn clause, discussed later in this guide.

Since modifies clauses are a type of postcondition, they are also only allowed on opaque procedures.