Modeling partiality by nondeterminism - from abstract specifications to flexible error handling

Yngve Lamo and Michal Walicki

Reports in Informatics No. 178, August 1999, Department of Informatics, University of Bergen, Norway.


The paper presents a new way to model partial operations by use of nondeterminism: a partial operation is modeled as a nondeterministic operation returning, possibly, any value of the carrier. We introduce an institution of multialgebras $\inst{MA}$ (modelling nondeterministic operations by set-valued functions) and illustrate the flexibility of our approach by examples showing uniform treatment of strictness, non-strictness and various error handling. We present a methodology for specification development from an abstract specification to low level error handling. We also study the conditions for $\inst{MA}$ specifications to ensure the existence of initial models. Finally we relate $\inst{MA}$ to other institutions, in particular, we show embedding of partial algebras and membership algebras into $\inst{MA}$. Applying institution transformation instead of embedding leads to the possibility of resuing partial algebra specifications in the proposed framework -- a partial algebra specification can be conservatively (preserving the models) imported to $\inst{MA}$ while the extension of the model class allows for furhter development towrds explicit error treatement.