4.4. Preconditions🔗

A precondition, written with requires, states what must be true when a procedure is called. It has two effects. It restricts callers: every call site must prove the precondition holds for the arguments it passes. And it gives the body an assumption to work from when proving its own obligations.

procedure halve(x: int) returns (r: int)
  requires x > 0
  opaque
  ensures r >= 0
{
  r := x / 2
};

procedure caller()
  opaque
{
  var a: int := halve(10);   // ok: 10 > 0
  var b: int := halve(0)     // error: precondition does not hold
};

A procedure may have several requires clauses; they are conjoined. A call must satisfy all of them.

procedure addBoth(x: int, y: int) returns (r: int)
  requires x > 0
  requires y > 0
  opaque
  ensures r > 0
{
  r := x + y
};