We look at a simple language with an exception mechanism:
S → throw id
S → S catch id ⇒ S
S → S or S
S → other
A throw statement throws a named exception. This is caught by the nearest enclosing catch statement (i.e., where the throw statement is in the left sub-statement
of the catch statement) using the same name, whereby the statement after the arrow in the catch statement is executed. An or statement is a non-deterministic
choice between the two statements, so either one can be executed. other is a statement that do not throw any exceptions.
We want the type checker to ensure that all possible exceptions are caught and
that no catch statement is superfluous, i.e., that the exception it catches can, in
fact, be thrown by its left sub-statement.
Write type-check functions that implement these checks. Hint: Let the type of a
statement be the set of possible exceptions it can throw.