4.1. Assertions🔗

An assert states a fact that Laurel must prove holds at that point in the program. If the solver cannot prove it, verification fails and the failing assert is reported.

procedure checkPositive(x: int)
  requires x > 0
  opaque
{
  assert x > 0;
  assert x >= 1
};

The dual of assert is assume. An assume introduces a fact without proof: from that point on, Laurel reasons as if the assumed expression is true. Assuming something false makes everything afterwards trivially provable, which is occasionally useful but should be used with care.

procedure assumeThenProve()
  opaque
{
  assume false;
  assert false  // provable: we assumed a contradiction
};

Assertions are the building block behind every other verification feature in this guide. Preconditions, postconditions, and loop invariants are all ultimately checked by turning them into assertions at the right program points.