4.11.1. Declaring and throwing🔗

throws T in a procedure's signature says the procedure may finish by throwing a T. In the body, throw e raises e and abandons the rest of the procedure.

composite Exception {}
composite ArithmeticException extends Exception {}

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

throws is part of the signature — it changes what callers have to deal with — so it sits with returns, before opaque.

4.11.2. Uncaught exceptions🔗

A procedure declaring throws T may only let exceptions escape whose type is a subtype of T. This is checked statically:

composite ArithError {}
composite ParseError {}

procedure wrongThrows()
  throws (e: ArithError)
  opaque
{
  var e: ParseError := new ParseError;
  throw e
  // error: procedure 'wrongThrows' may throw 'ParseError', which is not a
  // subtype of its declared `throws` type 'ArithError'
};

A procedure that declares no throws may not let any exception escape, whether thrown directly or propagated from a callee. This is checked by the verifier, so it is an error only if the exception can actually escape: an uncaught throw is asserted to be unreachable, and an uncaught call to a throwing procedure is asserted not to throw, which the callee's throwsOn cases decide.

composite Boom {}

procedure checked(x: int) returns (r: int)
  requires x >= 0
  opaque
{
  if x < 0 then {
    var b: Boom := new Boom;
    throw b   // verifies: unreachable under the precondition
  };
  r := x
};

Without the precondition the throw is reported as uncaught exception 'Boom' is not thrown does not hold. An exception that reaches the end of an outermost try uncaught — no catch matched — is checked when it leaves the try, since the try could still have intercepted it, and is reported at the throw (or throwing call) it came from.

Whether the source language requires declaring exceptions is a separate question: procedures coming from Python or JavaScript can carry a throws clause too, even though neither language has that surface construct.

4.11.3. Inferred throws🔗

throws (e: inferred) lets Laurel compute the thrown type: it becomes the common supertype of every exception that may escape the body uncaught, including those propagated from callees (whose own inferred types are computed together with it). throws (e: T inferred) keeps a declared T and joins the inferred types with it. When nothing escapes, the procedure declares no throws; when the escaping types have no common supertype, it is an error.

composite ArithError {}

procedure div(a: int, b: int) returns (r: int)
  throws (e: inferred)   // inferred: throws (e: ArithError)
  opaque
{
  if b == 0 then {
    var x: ArithError := new ArithError;
    throw x
  };
  r := a / b
};

This is how a frontend lets unchecked exceptions propagate without declaring them: the obligation moves from the thrower to its callers, as for a declared throws.

Each procedure is inferred from its own body. An override is capped at the type of the method it overrides, so a call through the base never sees more than the base's type: what the override lets escape within that type stays in its throws, and the rest is asserted not to happen, as in a procedure without throws. An override may throw less than its base, or nothing. A procedure without a body cannot have an inferred clause; its type must be declared. A procedure with throwsOn cases must not have its declared type widened by inference, because the cases' binding would widen with it; that is an error.

4.11.4. Handling: try, catch, finally🔗

catch dispatches on a predicate rather than on a type, written catch e when <condition on e>. Type-based dispatch is one such predicate: catch e when e is NotFound. Clauses are ordered and first-match-wins, and a clause with no when guard is a catch-all. finally runs on the way out of the try.

composite Exception {}
composite NotFound extends Exception {}
composite Invalid extends Exception {}

procedure handle(fail: int) returns (r: int)
  opaque
{
  r := 0;
  try {
    if fail == 1 then {
      var e: NotFound := new NotFound;
      throw e
    };
    if fail == 2 then {
      var i: Invalid := new Invalid;
      throw i
    }
  } catch e when e is NotFound {
    r := 1
  } catch e {
    r := 2
  } finally {
    assert r >= 0
  }
};

finally runs after a normal completion, after a caught exception, on the way out with an uncaught one, and when a handler itself throws or returns. A return or an exit that leaves the try runs it too, and nested finally arms chain outward.

One rule decides the rest: if the finally arm itself completes abruptly — it returns, throws, or exits — that completion wins, and whatever was pending is discarded. This is Java's rule (JLS 14.20.2), so try { throw e } finally { return } returns normally and the exception is gone.

4.11.5. The type of a catch binding🔗

A catch binding is typed at the least common ancestor of the exception types that can reach it: the types thrown directly in the try body, and the declared throws types of the procedures the body calls. When those share a common ancestor T, the binding has type T, and reading a field of e needs no downcast.

composite Exception {
  var message: string
}
composite NotFound extends Exception {}
composite Invalid extends Exception {}

procedure logFailure(which: int) returns (out: string)
  opaque
{
  out := "";
  try {
    if which == 1 then {
      var f: NotFound := new NotFound;
      f#message := "missing";
      throw f
    };
    var i: Invalid := new Invalid;
    i#message := "invalid";
    throw i
  } catch e {
    // `NotFound` and `Invalid` join at `Exception`, so `e` is an `Exception` and
    // the inherited field is readable without a cast.
    out := e#message
  }
};

In a guarded clause the binding has the type its guard tests, or for a multi-catch guard e is A || e is B their least common ancestor, when that is narrower: under catch e when e is NotFound, e is a NotFound.

If the types reaching a catch share no common ancestor, Laurel reports an error rather than leaving the binding untyped. If the body throws nothing determinable, no exception can reach the clauses, and they are dropped as unreachable.

A guard may test the binding against a type unrelated to the binding's type, as a Java multi-catch arm for an unchecked exception the body never throws does: catch e when e is StateError || e is NotFound. Such a test can never be true, so it is accepted and treated as false, and the other tests in the guard still catch. A clause whose guard is only such tests, or a disjunction of them, can never catch: its body is not checked.

A frontend that needs to catch values with no useful common ancestor — unrelated types, or JavaScript's arbitrary thrown values — can box them: wrap the value in a composite field when throwing, and unwrap it in the handler.

4.11.6. Not yet supported🔗

Two shapes are rejected during resolution with a not yet supported diagnostic rather than lowered, because the alternatives would be an internal error or a silent miscompile:

• a call to a procedure that throws in a nested expression position. Only a whole statement or a whole assignment right-hand side is handled, so s := f() is fine while s := 1 + f() is rejected;

• a catch handler that re-declares its own exception binding, because the substitution that rewrites the binding matches by name and is not scope-aware.