Link Search Menu Expand Document
CBS-beta

Funcons-beta : Breaking.cbs | PRETTY | PDF

Breaking 

[
  Datatype breaking
  Funcon   broken
  Funcon   finalise-breaking
  Funcon   break
  Funcon   handle-break
]
Meta-variables
  T <: values
Datatype
  breaking ::= broken

broken is a reason for abrupt termination.

Funcon
  finalise-breaking(X:=>T) : =>T|null-type
   ~> finalise-abrupting(X)

finalise-breaking(X) handles abrupt termination of X due to executing break.

Funcon
  break : =>empty-type
   ~> abrupt(broken)

break abruptly terminates all enclosing computations until it is handled.

Funcon
  handle-break(_:=>null-type) : =>null-type

handle-break(X) terminates normally when X terminates abruptly for the reason broken.

Rule
                X --abrupted( )-> X′
  ------------------------------------------------
  handle-break(X) --abrupted( )-> handle-break(X′)
Rule
                X --abrupted(broken)-> _
  ---------------------------------------
  handle-break(X) --abrupted( )-> null-value
Rule
                X --abrupted(V:~breaking)-> X′
  ------------------------------------------------
  handle-break(X) --abrupted(V)-> handle-break(X′)
Rule
  handle-break(null-value) ~> null-value
From the PLanCompS Project CBS-beta issues… Suggest an improvement…

← ↑ →