Laurel User Guide

6.5. Exceptional contracts🔗

requires and ensures describe the entry condition and the normal return. A procedure that can throw has a second exit, described by one or more throwsOn behavior cases. They follow opaque, alongside ensures and modifies, because they constrain an exit rather than form part of the signature.

A case pairs a pre-state guard with the contract for the throwing path it selects:

composite Exception {}
composite ArithmeticException extends Exception {}

procedure div(a: int, b: int) returns (r: int)
  throws (e: Exception)
  opaque
  throwsOn b == 0 {
    ensures e is ArithmeticException
  }
{
  if b == 0 then {
    var ae: ArithmeticException := new ArithmeticException;
    throw ae
  };
  r := a / b
};

The guard forces the throw. If b == 0 holds on entry the procedure is guaranteed to exit by throwing, and the thrown value satisfies the case's ensures clauses. So a caller can prove ahead of time that a given input will fail, and knows what it will get.

throws (e: T) names the thrown value as well as its type, and scopes that name over every case's ensures. There is one spelling, always binding: a procedure that says nothing about its exception today would otherwise have to change its signature the moment it wants to. e is deliberately not in scope in a requires, in a top-level ensures, or in a guard — all three are evaluated where no exception exists.

The declaration already tells callers what was thrown. throws (e: T) on its own guarantees

it threw ==> e is T

on every throwing path, so a case never has to restate the declared type. That is why the example above says ensures e is ArithmeticException and not ensures e is Exception: a case's type test earns its place only when it narrows the declaration to a subtype for that particular path. Restating the declared type would in fact say less, since the case's ensures holds only when that case's guard held, while the declaration holds always.

A case with nothing left to say may therefore be empty, and is still meaningful — its guard alone forces the throw:

composite Exception {}

procedure mustThrow(a: int, b: int) returns (r: int)
  throws (e: Exception)
  opaque
  throwsOn b == 0 {
  };

A caller passing b == 0 learns that the call throws, and learns from the declaration that what it gets is an Exception.

Stating cases also settles the converse. Because a guard forces its throw, writing any case is a claim to have enumerated them, so the verifier checks

it threw ==> one of the guards held

A caller that can refute every guard therefore learns the call cannot have thrown. Two consequences worth knowing: a throwing path that matches no guard is reported rather than quietly accepted, and the two boundary cases read as you would hope — throwsOn true { … } means the procedure always throws, and throwsOn false { } means it never does.

None of this is documentation only. For a procedure with a body the verifier proves the body honours the cases; at a call site they are assumed, so a caller can reason about a throwing procedure without seeing its code.

6.5.1. What a case may contain🔗

A case takes ensures and modifies, mirroring their normal-exit counterparts but scoped to the path its guard selects. An ensures inside a case also takes summary "…", exactly as a top-level one does, so a failing exceptional postcondition can report in your words:

  throwsOn b == 0 {
    ensures e is ArithmeticException summary "dividing by zero throws"
  }

Two forms that exist on the normal exit are deliberately absent inside a case, so a parse error there is the surface telling you to write something else:

  • No free or checked variant of a case's ensures. This is a deferral rather than a rule about exceptions; until it lands, a case's ensures is always both checked against the body and assumed by callers.

  • No modifies *. It would say nothing new: a case that names no modifies already leaves its throwing path unframed, which is exactly what the wildcard means on the normal exit. Write throwsOn C { } — or omit the modifies and keep the ensures — instead.

The reasoning behind both is in the exceptions section of the Laurel Designer Guide.

6.5.2. Stating no case🔗

Cases are optional, and omitting them is not the same as throwsOn false. A procedure with no case makes no claim about its throwing paths at all:

composite Err {}

procedure thrower(x: int) returns (r: int)
  throws (e: Err)
  opaque
{
  if x < 0 then {
    var e: Err := new Err;
    throw e
  };
  r := x
};

A caller of thrower learns exactly one thing about the throwing exit — that what comes out is an Err, from the declaration. It cannot tell when the call throws, so it must allow for both exits; and because no case names a frame, it must also assume the heap may have changed. Nothing is checked against the body either: with no guards to enumerate, the it threw ==> one of the guards held obligation is not emitted.

That is weaker than stating a case, but it is weak in the safe direction — the contract claims nothing, so nothing it claims can be wrong. The dangerous shape is partial enumeration, cases with a gap between them, and that is what the check above catches.

Saying nothing is the right choice when the throwing condition is not expressible in the procedure's own pre-state. The clearest example is a procedure that propagates a callee's exception: it throws exactly when the callee does, and the callee's contract need not say when that is. Where the condition is available — as x < 0 is to thrower — stating a case is strictly more informative, and worth doing.