A typical complaint of users of formal verification tools is the cost of adding the necessary annotations, in the form of contracts, loop invariants, or others. While some of these annotations are expected to state the desired behavior of the program, some are only here to help the tools, and should ideally be generated.

We have just implemented a similar feature for functional contracts, that saves the effort to add preconditions and postconditions to subprograms. This feature is only available for the analysis of local subprograms, for which the analyzer knows all the call sites. Instead of analyzing the subprogram in all the contexts allowed by its precondition (which requires that a user writes such a precondition), GNATprove now analyzes the subprogram in all the contexts where it is effectively called! As a result, the precision of the analysis of callers is much improved as well, as it does not depend on the precision of the given postcondition (which also requires that a user writes such a postcondition). Very simple but a potential huge time/cost saver for users.

See the User's Guide for a detailed example.

This makes it also far easier to refactor code, as local subprograms can be introduced to factor out common tasks, or to separate actions in named logical blocks, without requiring that the user also spends time writing contracts on the new subprograms.

Note that this feature is not in the SPARK GPL 2014 release. It will be in the release scheduled for 2015.