6.3. 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.