2.2. Verification🔗

To achieve goal 1.2, enable proving properties through verification, Laurel has the following features.

2.2.1. Assertions🔗

An assert states a property that must hold at the point where it appears. An assertion is the basic unit of proof: everything else in this section is a way of making the facts an assertion needs available, or of stating such properties more conveniently.

procedure abs(x: int) returns (r: int)
{
    if x < 0 then { r := -x } else { r := x };
    assert r >= 0
};

Here the assertion holds on both branches, so it is discharged; had a branch left r negative, the assertion would report a failure.

2.2.2. Quantifiers🔗

Laurel supports universal (forall) and existential (exists) quantifiers in properties, written forall(x: T) => P(x) and exists(x: T) => P(x). They let a single property range over unboundedly many values.

procedure allNonNegativeSquares()
  opaque
{
    assert forall(x: int) => x * x >= 0
};

procedure someMultipleOf42()
  opaque
{
    assert exists(x: int) => x == 42
};

The two quantifiers correspond to the two analysis modes. A universal quantifier is what soundness (correctness) checking needs: to prove a procedure correct, its properties must hold for all inputs and all reachable states, so proving a forall establishes the property for every case. An existential quantifier fits bug finding (incorrectness) mode: exhibiting some state that satisfies a property is enough to witness that a situation is reachable, for example a state that violates an intended invariant. Because unrestricted quantifier instantiation is a common cause of slow verification, a forall may carry an explicit trigger, written forall(i: int) { P(i) } => …, that tells the solver which terms may instantiate it.

2.2.3. Old🔗

In a postcondition, old(e) denotes the value of the expression e in the procedure's pre-state, before the body ran. This lets a contract relate the final state to the initial one, which is how mutation is specified. The specification is written in a mutation-free style: old and the current value are both just expressions, and comparing them describes the effect of the mutation without the contract itself performing any mutation.

procedure increment(counter: Counter)
  opaque
  ensures counter#value == old(counter#value) + 1
  modifies counter
{
  counter#value := counter#value + 1
};

The postcondition counter#value == old(counter#value) + 1 captures the mutation performed by the body, yet it is a pure comparison between two values. A caller learns exactly how the field changed relative to its prior value without the contract mutating anything, keeping verification code erasable (see goal 7).

2.2.1.	Assertions
2.2.2.	Quantifiers
2.2.3.	Old