A New Notion of Partial Correctness for Exception Handling. Sekerinski, E. & Zhang, T. In Bonakdarpour, B. & Maibaum, T., editors, Proceedings of the 2nd International Workshop on Logical Aspects of Fault-Tolerance, pages 116–132, June, 2011.
A New Notion of Partial Correctness for Exception Handling [pdf]Paper  abstract   bibtex   
We study the correctness of programs that use exception handling to deal with failures. A new notion of partial correctness is introduced for the design of programs that can continue safely after an unanticipated failure. Partial correctness is contrasted with total correctness though their verification rules. These rules are derived from a definition of statements with exceptions as higher order predicate transformers. The use of total and partial correctness is illustrated with three design patterns, rollback, degraded service, and recovery block.

Downloads: 0