Generic Exception Handling and the Java Monad

Abstract. We develop an equational definition of exception monads that characterizes Moggi’s exception monad transformer. This axiomati-zation is then used to define an extension of previously described monad-independent computational logics by abnormal termination. Instantiat-ing this generic formalism with the Java monad used in the LOOP project yields in particular the known Hoare calculi with abnormal termination and JML’s method specifications; this opens up the possibility of extend-ing these formalisms by hitherto missing computational features such as I/O and nondeterminism