Refining exceptions using King and Morgan´s exit construct

In this paper we discuss the refinement of exceptions. We extend the Guarded Command Language normally used in the refinement calculus, with a simple exception handling statement, which we model using King and Morgan´s exit statement (1995). We derive some variants of King and Morgan´s refinement laws for their exit statement, and illustrate the approach with an example of a refinement of a simple program.