4.6. Quantifier🔗

For specifications that range over many values, Laurel provides quantifiers. A forall states that its body holds for every value of the bound variables; an exists states that there is at least one value for which the body holds. Both take one or more typed binders and a body introduced with =>.

procedure quantifiers()
  opaque
{
  assert forall(x: int) => x + 0 == x;
  assert exists(x: int) => x == 42
};

The implication operator ==> is frequently used inside quantifiers to restrict the range of interest — for instance, to say something about every index of an array within bounds:

procedure inContract(n: int)
  requires n > 0
  opaque
  ensures forall(i: int) => i >= 0 ==> i < n ==> i < n + 1
{
};

Because a forall over an infinite domain (such as all integers) cannot be checked by enumeration, the solver reasons about it logically. To control how it instantiates a quantifier, you can attach a trigger — a pattern in braces that tells the solver which terms should cause the quantified fact to fire:

procedure P(x: int): int;
procedure withTrigger()
  opaque
{
  assume forall(i: int) { P(i) } => P(i) == i + 1;
  assert P(1) == 2   // the term P(1) matches the trigger, so the fact fires
};