A Unifying Theory of Multi-Exit Programs

Abstract

<p>Programs have multiple exits in the presence of certain control structures, e.g., exception handling and coroutines. These control structures offer flexible manipulations of control flow. However, their formalizations are overall specialized, which hinders reasoning about combinations of these control structures.</p> <p>In this thesis, we propose a unifying theory of multi-exit programs. We mechanically formalize the semantics of multi-exit programs as indexed predicate transformers, a generalization of predicate transformers by taking the tuple of postconditions on all exits as the parameter. We explore their algebraic properties and verification rules, then define a normal form for monotonic and for conjunctive indexed predicate transformers. We also propose a new notion of fail-safe correctness to model the category of programs that always maintain certain safe conditions when they fail, and a new notion of fail-safe refinement to express partiality in software development.</p> <p>For the indexed predicate transformer formalization, we illustrate its applications in three models of multi-exit control structures: the termination model of exception handling, the retry model of exception handling, and a coroutine model. Additionally, for the fail-safe correctness notion and the fail-safe refinement notion, we illustrate their applications in the termination model. Six design patterns in the termination model and one in the retry model are studied. All the verification rules and design patterns in the thesis have been formally checked by a verification tool.</p>