4.3. Exceptional contracts🔗

A procedure that can throw has two ways to finish, and modular verification needs both of them described. ensures and modifies say nothing about the throwing exit, so without further clauses a caller that catches an exception would know nothing at all about the state it caught it in — the same loss of precision that opaque heap mutation has without a modifies clause. Laurel therefore mirrors each normal-exit clause on the exceptional exit.

A throwsOn C { … } case describes one throwing path. Its guard C is evaluated in the pre-state but is deliberately not an obligation on the caller: the case states that if C held on entry then the procedure is guaranteed to throw, and the case's ensures clauses hold of the thrown value. That is what lets a caller prove ahead of time that a particular input fails. Inside a case, ensures and modifies mirror their normal-exit counterparts, scoped to that path — so a procedure may legitimately touch a log object only when it fails, and say which one for which failure.

Because a guard forces its throw, stating any case is a claim to have enumerated them, and Laurel checks the converse: it threw ==> one of the guards held. That is what gives a caller the other direction, letting it rule the throwing exit out rather than only characterise it. It also means a throwing path matching no guard is reported instead of being left silently unconstrained, since every case's frame is vacuous on such a path.

A frontend does not need to emit a type test for the declared exception type. throws (e: T) already yields it threw ==> e is T on every throwing path, so a case's ensures e is U is worth emitting only when U is a proper subtype of T — narrowing the declaration for that path. Restating T itself would be weaker, not redundant: the case's ensures is conditioned on the case's guard, while the declaration holds unconditionally. A case that has nothing to narrow can be empty, and still carries its forcing claim.

The cost of keying cases on a pre-state guard is that framing a throwing path requires naming its condition. A procedure whose throwing condition is not expressible in its own pre-state — one that propagates a callee's exception, for instance — must leave that path unframed by stating no case, which is the modular-verification loss described above. Weigh that when designing a frontend's contract emission: prefer emitting a case whenever the condition is available.

One restriction on guards is worth knowing when emitting them: a guard may not read the heap. It may name parameters and call heap-independent procedures, but a field access (x#f) or a call to a heap-reading procedure is rejected. The reason is an implementation gap rather than a design choice — a guard is lowered into a postcondition, which is evaluated in the post-state, so a heap-reading guard would silently mean "held on exit" instead of "held on entry". A frontend that needs to test heap state in a guard hoists the read into a parameter and ties it to the field with a requires, which is exactly what a Java frontend does for an array-bounds check: take the length as an argument and guard on that.

As with the normal-exit clauses, cases are checked against the body when there is one and assumed at call sites, which is what keeps a throwing procedure verifiable independently of its callers.

The mirroring of normal-exit clauses is deliberately not total, and the three gaps are worth recording so a frontend author does not read them as oversights.

A case's ensures accepts summary "…", exactly as a normal ensures does, so an exceptional postcondition can be phrased in the frontend's own words rather than Laurel's.

There is no wildcard case frame, because an empty one already means what a wildcard would. A normal modifies * is encoded by emitting no frame at all — the procedure may change anything — and a case that names no modifies is likewise given no frame, leaving its throwing path unconstrained. So throwsOn C { modifies * } would be a second spelling of throwsOn C { }, and the surface omits it rather than offering two ways to say one thing. This is also why stating a case with only an ensures does not tighten the frame on that path: heap framing is opt-in per case. The lowering normalizes the wildcard to "no frame" rather than relying on the surface to exclude it, because ThrowsOnBlock is public AST: a frontend can build a wildcard case frame even though no syntax produces one, and the frame builder would otherwise read an empty target list as "nothing changed" — the exact inverse.

There are no free or checked variants of a case's ensures. This one is a deferral rather than a principle: the underlying condition already carries a mode, the lowering already preserves an authored one, and a bodiless procedure's cases are already assumed rather than checked. What remains is grammar and one decision — whether free should also relax the case's forcing claim. It should not: a free forcing claim would assert nothing about the body, which is the one thing a case exists to do.