Reasoning About Subprogram Termination in SPARK

The Ada language is designed for safety critical applications. However, most of its safety-oriented features - language mandated checks and contract based programming in particular - rely on dynamic checks. The SPARK tool performs formal proof of Ada programs, verifying their correctness for all possible inputs. It verifies statically both the language mandated checks and conformance to user-provided contracts. The analysis performed by SPARK is modular, operating on a per-subprogram basis. To model interactions between subprograms, it relies on contracts, making it necessary for users to annotate their subprograms carefully. Preconditions define the valid calling contexts, they are assumed when verifying the subprogram, and checked on calls. Conversely, postconditions summarize the effect of a subprogram call when it returns normally. They are checked when the subprogram is verified, and assumed when verifying callers. As the analysis is modular, only the information that is explicit in the postcondition of a subprogram will be known when verifying callers [1].