On the laws of failure: a theory of compensable programs

Author

Marmsoler, Diego

Author_Institution

Tech. Univ. Munchen, Munich, Germany

fYear

2013

fDate

1-4 July 2013

Firstpage

2146

Lastpage

2151

Abstract

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.

Keywords

error handling; programming theory; system recovery; theorem proving; Isabelle/Isar; algebraic reasoning; compensable program theory; direct consequences; error handling; exception handling; failure laws; inverse program; long-running transactions; program commonalities; program differences; proof obligation; recovery blocks; trace semantics; Cognition; Computer languages; Interference; Programming; Semantics; Standards; Syntactics; Algebraic approaches to semantics; Denotational semantics; Error handling and recovery; Standards;

fLanguage

English

Publisher

ieee

Conference_Titel

EUROCON, 2013 IEEE

Conference_Location

Zagreb

Print_ISBN

978-1-4673-2230-0

Type

conf

DOI

10.1109/EUROCON.2013.6731014

Filename

6731014