On the laws of failure: a theory of compensable programs

This work identifies three basic programming concepts used for error handling and investigates the laws governing these concepts. A trace semantics for exception handling, long-running transactions and recovery blocks is given and 11 basic laws are derived. Algebraic reasoning is used to derive three more properties on top of these basic laws. An assumption about the existence of an inverse program is investigated and two direct consequences are provided. The assumption is weakened to address practical issues and a proof obligation is provided to obtain the properties anyway. The work is based on the algebraic method and provides a novel approach to completely specify a program in terms of commonalities and differences w.r.t. another program. Furthermore, all proofs are stated exclusively in Isabelle/Isar, thus they are mechanically checked, though human readable.