4.5.1. Arithmetic🔗

+, -, *, unary -, /, %, /t, and %t operate on numeric values, and both operands must have the same numeric type. For integers there are two division/remainder pairs, and the difference only shows up on negative operands:

• / and % are Euclidean: the remainder is never negative;

• /t truncates the quotient toward zero, and %t is a - b * (a /t b).

procedure divisionFacts()
  opaque
{
  assert -7 / 3 == -3;
  assert -7 % 3 == 2;
  assert -7 /t 3 == -2;
  assert -7 %t 3 == -1
};

All four forms generate a nonzero-divisor proof obligation, so a possible division by zero shows up as a failed precondition at the offending operator rather than as undefined behaviour. There is no source syntax for skipping that check.

Operators are not a separate kind of expression: each is a call to an overloaded built-in procedure, which is why operand admissibility is overload selection and why / can carry a precondition at all. That mechanism is described under Operators.

4.5.2. Boolean operators🔗

procedure booleans(a: bool, b: bool)
  opaque
{
  assert (a & b) == (b & a);      // eager: both sides evaluated
  assert (a | b) == (b | a);      // eager
  assert (a && b) == (b && a);    // b evaluated only when a is true
  assert (a || b) == (b || a);    // b evaluated only when a is false
  assert (a ==> b) == (!a || b);  // b evaluated only when a is true
  assert !(!a) == a
};

The eager and short-circuiting pairs differ only when the right-hand side has an effect, which in Laurel it may: operands can contain assignments and calls. The short-circuit forms mean exactly what the corresponding conditional means — a && b is if a then b else false, a || b is if a then true else b, and a ==> b is if a then b else true.

One caveat: if the right-hand side contains an assert or assume and nothing else effectful, write the conditional explicitly rather than relying on the short-circuit form, because the proof statement can currently escape its guard.

4.5.3. Equality, ordering, and strings🔗

procedure comparisons(x: int, y: int, l: string, r: string)
  opaque
{
  assert (x == y) == !(x != y);
  assert (x < y) ==> (x <= y);
  assert (x > y) ==> (x >= y);
  assert (l ^ r) == (l ^ r)
};

Equality requires operands of consistent types and is available at every type. Ordering requires numeric operands. ^ concatenates two strings.

Equality means different things at different types, and the difference matters: on a datatype it is structural, and on a composite it is reference identity. See Aliasing and separation.