====================================================
V, U ::= ...usual values like integers and booleans...
| E(U) (exception)
| fun f x => M (function)
M, N ::= ...usual arithmetic and relational operators...
| x
| E(M) (exception)
| M N
| raise M (throw in Java)
| M handle E1(x1) => N1 | ... | En(xn) => Nn (try-catch block in Java)
====================================================
Evaluation:
M evals U
--------------
(E(M)) evals (E(U))
M evals V
------------------
(raise M) raises V
M evals V
----------------------------------------------------
(M handle E1(x1) => N1 | ... | En(xn) => Nn) evals V
M raises Ei(U)
(Ni with xi:=U) evals V
----------------------------------------------------
(M handle E1(x1) => N1 | ... | En(xn) => Nn) evals V
M raises Ei(U)
(Ni with xi:=U) raises V
-----------------------------------------------------
(M handle E1(x1) => N1 | ... | En(xn) => Nn) raises V
M raises E(U)
E != E1 ... E != En
--------------------------------------------------------
(M handle E1(x1) => N1 | ... | En(xn) => Nn) raises E(U)
====================================================
Types:
Gamma(E) = (S->Exception)
Gamma |- M : S
-------------------------
Gamma |- E(M) : Exception
Gamma |- M : Exception
----------------------
Gamma |- (raise M) : T
Gamma |- M : T
Gamma(E1) = (S1->Exception) (Gamma,x1:S1): |- N1 : T
...
Gamma(En) = (Sn->Exception) (Gamma,xn:Sn): |- Nn : T
---------------------------------------------------------
Gamma |- (M handle E1(x1) => N1 | ... | En(x2) => Nn) : T
====================================================
