Formal Specifications

To help ensure proper operation, well-designed application programs include exception-handling routines to gracefully resolve any anomalous behavior by the application or its operating system. For that reason, programming languages and operating systems include mechanisms to catch unexpected or illegal events during run time and handle them outside the normal flow of control.

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.