A Normal Form for Multi-Exit Statements. Sekerinski, E. & Zhang, T. Technical Report McMaster University, 2011.
A Normal Form for Multi-Exit Statements [pdf]Paper  abstract   bibtex   
For a class of statements, a normal form provides a uniform way for their formal specification. Control structures like exception handling introduce additional exit(s) of statements, and new normal forms as a consequence. In this paper, we give the normal forms of several classes of multi-exit statements, explore their algebraic properties, and discuss their potential of being utilized for the development of programs, where a postcondition for each exit is required. All the theorems have been checked with a formal verification tool.

Downloads: 0