Exception handling allows (1) a program to be structured such that the original design is preserved in presence of possibly failing components; (2) rare or undesired cases to be treated in an unobtrusive manner; and (3) imperfections to be handled systematically. This chapter develops a theory of exception handling with try-catch statements, and demonstrates its use in the design of dependable systems by giving a formal account of the patterns of masking, propagating, flagging, rollback, degraded service, recovery block, repeated attempts, and conditional retry. The theory is based on weakest exceptional preconditions, which are used for both defining statements and proofs. Proof outlines are introduced and used to establish the correctness of the patterns.
