CSC448: Exceptions: Syntax and Operational Semantics [7/12]

A simple functional language with exceptions, where we assume a fixed set of exception names.

V    ::= ...usual values like integers and booleans...
       | E                                    (exception name, no args) 
       | fun f x => M                         (function)

M, N ::= ...usual arithmetic and relational operators...
       | x
       | M N
       | raise M                              (throw in Java)
       | M handle E1 => N1 | ... | En => Nn   (try-catch block in Java)

We can give an operational semantics that describes the runtime behaviour of such programs using two judgement forms:

• M evals V
• M raises V

====================================================
Values:

  ---------
  V evals V

Function application:

  M evals (fun f x => M')
  N evals V
  --------------------------------------------- 
  (M N) evals (M' with x:=V, f:=(fun f x =>M'))

  M raises V
  --------------
  (M N) raises V

  M evals (fun x => M')
  N raises V
  ---------------------
  (M N) raises V

Raise/Handle:

  M evals V
  ------------------
  (raise M) raises V

  M evals V
  --------------------------------------------
  (M handle E1 => N1 | ... | En => Nn) evals V

  M raises Ei
  Ni evals V
  --------------------------------------------
  (M handle E1 => N1 | ... | En => Nn) evals V

  M raises Ei
  Ni raises V
  ---------------------------------------------
  (M handle E1 => N1 | ... | En => Nn) raises V

  M raises V
  V != E1  ...  V != En
  ---------------------------------------------
  (M handle E1 => N1 | ... | En => Nn) raises V


====================================================
Variables:

  Gamma(x) = T
  --------------
  Gamma |- x : T

Functions:

  (Gamma, (f:(S->T)), (x:S)) |- M : T
  -----------------------------------
  Gamma |- (fun f x => M) : (S->T)

  Gamma |- M : (S->T)
  Gamma |- N : S
  --------------------------------
  Gamma |- (M N) : T

Exceptions:

  ----------------------
  Gamma |- E : Exception

  Gamma |- M : Exception
  ----------------------
  Gamma |- (raise M) : T

  Gamma |- M : T
  Gamma |- N1 : T   ...   Gamma |- Nn : T
  -------------------------------------------------
  Gamma |- (M handle E1 => N1 | ... | En => Nn) : T

====================================================