Refining Exceptions in Four-Valued Logic?

Abstract. This paper discusses refinement of programs that may raise and catch exceptions. We show that exceptions are expressed by a class of predicate trans-formers built on Arieli and Avron’s four-valued logic and develop a refinement framework for the four-valued predicate transformers. The resulting framework enjoys several refinement laws that are useful for stepwise refinement of programs involving exception handling and partial predicates. We demonstrate some typi-cal usages of the refinement laws in the proposed framework by a few examples of program transformation.