Equational Theories of Abnormal Termination Based on Kleene Algebra.

We study at an abstract level imperative while programs with an explicit fail operation that causes abnormal termination or irreparable failure, and a try-catch operation for error handling. There are two meaningful ways to define the semantics of such programs, depending on whether the final state of the computation can be observed upon failure or not. These two semantics give rise to different equational theories. We investigate these two theories in the abstract framework of Kleene algebra, and we propose two simple and intuitive equational axiomatizations. We prove very general conservativity results, from which we also obtain decidability and deductive completeness of each of our calculi with respect to the intended semantics.