5.7. Contract well-formedness🔗

An assertion inside a contract must be proven, and that includes the implicit assertions — the ones you did not write, such as the precondition of a call the clause makes. A contract clause is an expression, so it carries the obligations of every operation it names, exactly as the same expression would in a procedure body.

Two kinds of obligation come up. A partial operation raises the one it always raises: division needs a nonzero divisor, a sequence index needs to be in bounds. And a call must satisfy the callee's preconditions.

The clause's mode does not change any of this. free and checked choose where the clause's own condition is asserted and assumed; neither suppresses the obligations of the expression that states it. A failure is reported at the clause, and the procedure whose contract it is must discharge it — not the caller.

5.7.1. Order matters🔗

A clause may rely on the clauses written before it to discharge its obligations, so where a guard sits decides whether the clause that needs it is well-formed. Division requires a nonzero divisor, so the second clause below is fine only because the first has already ruled out x == 0:

procedure scaleDown(x: int) returns (r: int)
  requires x != 0
  requires 10 / x > 1
  opaque
{
  r := x
};

Written the other way round, the division comes before anything constrains x, so the divisor may be zero and Laurel reports precondition does not hold on 10 / x:

procedure scaleDownBadOrder(x: int) returns (r: int)
  requires 10 / x > 1
  requires x != 0
  opaque
{
  r := x
};

An ensures may additionally rely on the procedure's preconditions, whatever their mode. Since the requires clauses are conjoined, order changes nothing about what a caller must prove; it changes only which facts are in scope while Laurel checks a clause's own obligations.

5.7.2. A call in a clause🔗

The same rule covers a call, whose precondition has to be established at the clause just as it would at any other call site. Here the procedure's own requires is what discharges it:

procedure needsBig(x: int) returns (s: int)
  requires x > 100
  opaque
  ensures s == x + 1
{
  s := x + 1
};

procedure callsItSafely(x: int) returns (r: int)
  requires x > 100
  opaque
  free ensures r == needsBig(x)
{
  r := x + 1
};

Drop that requires and the call is no longer justified, so the clause fails even though it is free — the mode waives proving the condition, not the obligations inside it:

procedure needsBigAgain(x: int) returns (s: int)
  requires x > 100
  opaque
  ensures s == x + 1
{
  s := x + 1
};

procedure callsItUnsafely(x: int) returns (r: int)
  opaque
  free ensures r == needsBigAgain(x)
{
  r := x + 1
};