1.1. A first program🔗

A Laurel program is a sequence of declarations. The most important one is the procedure. A procedure has input parameters, optional output parameters introduced with returns, an optional contract, and a body enclosed in braces. Statements inside the body are separated by semicolons.

The procedure below computes integer division the hard way: it repeatedly subtracts the divisor from the dividend, counting how many times it can do so. The ensures clause then confirms the hand-rolled result against Laurel's built-in / operator, so the two must agree for the procedure to verify. The loop carries an invariant that ties the running quotient and remainder back to the original dividend — this is the fact the verifier needs to discharge the postcondition.

procedure divide(dividend: int, divisor: int) returns (quotient: int)
  requires dividend >= 0
  requires divisor > 0
  opaque
  ensures quotient == dividend / divisor
{
  var remainder: int := dividend;
  quotient := 0;
  while (remainder >= divisor)
    invariant remainder >= 0
    invariant dividend == quotient * divisor + remainder
  {
    remainder := remainder - divisor;
    quotient := quotient + 1
  };
  assert 0 <= remainder && remainder < divisor
};