by Lutz Schröder and Till Mossakowski
Abstract:
We develop an equational definition of exception monads that characterizes Moggi's exception monad transformer. This axiomatization is then used to define an extension of previously described monad-independent computational logics by abnormal termination. Instantiating 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 extending these formalisms by hitherto missing computational features such as I/O and nondeterminism.
Reference:
Lutz Schröder and Till Mossakowski: Generic exception handling and the Java monad, In Charles Rattray, Savitri Maharaj, Carron Shankland, eds.: Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, vol. 3116, pp. 443–459, Springer, 2004. [preprint]
Bibtex Entry:
@InProceedings{SchroderMossakowski04,
author = {Lutz Schr{\"o}der and Till Mossakowski},
title = {Generic exception handling and the {J}ava monad},
year = {2004},
editor = {Charles Rattray and Savitri Maharaj and Carron Shankland},
booktitle = {Algebraic Methodology and Software Technology},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3116},
pages = {443--459},
keywords = {Java monad dynamic logic exception HasCASL},
url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3116&spage=443},
comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/javapdl.pdf"> [preprint] </a>},
psurl = {http://www8.informatik.uni-erlangen.de/~schroeder/papers/javapdl.ps},
abstract = {We develop an equational definition of exception monads that
characterizes Moggi's exception monad transformer. This axiomatization
is then used to define an extension of previously described
monad-independent computational logics by abnormal
termination. Instantiating 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 extending these formalisms by hitherto missing
computational features such as I/O and nondeterminism.
},
}