One way that you can fortify your software's exception-handling ability is to harness formal specification statements. Intended for run-time verification of an application's design, formal specifications can be translated by a code generator into C, C++, or Java statements to be deployed for catching exceptions in the final product. Using formal specifications to generate exception-handling routines produces a robust hybrid program having multiple levels of recovery paths. The additional levels shield the application from worst-case scenarios that would otherwise crash it.
Such specification-based exception handling is a recent application of formal specifications to the world of real programs and applications. This paper described old and new applications of formal specifications, ranging from verification, through run-time rule checking, to run-time exception handling.