In SPARK 2014, we can write a function F and annotate it with a pre and a postcondition:

Let us look at how the SPARK 2014 proof tool handles a call to such a function. If F is called on C inside a program, then the tool checks that F_Pre (C) is true before the call and assumes that F_Post (C, Result) is true after the call. On an example,

is equivalent, for the proof tool, to

When the function is called in an assertion or in a contract, the tool works a bit differently. Indeed, when F is called on C, we still check that F_Pre is true on C but, instead of assuming that the postcondition holds for this particular instance, that is, F_Post (C, Result) is true, we rather use an axiom stating that the postcondition of F is always verified after a call. If X_Type is a range type, this amounts to assuming:

This allows an easier transformation as we do not need to make this assumption for each call but only once and for all before the verification of the caller. Note that, if F's contract was incorrect, this assumption may be false, or even unsound, which means that it can be used to prove anything. For example:

will lead to the obviously unsound assumption:

Because of this problem, up to releases SPARK Pro 14.1 or SPARK GPL 2014, GNATprove does not generate axioms for postconditions of normal functions, but only for definitions of expression functions. On the one hand, this restriction ensures that, if every expression function terminates, no false axiom can be generated (see this blog post). On the other hand, it reduces provability as, when a normal function is called in a contract or an assertion, the prover know nothing about it.

To alleviate this restriction, we have decided to also generate axioms for postconditions of non-mutually recursive normal functions.  Indeed, in this case, we can still ensure that no unsound axiom can be generated for a terminating, completely verified function. For example, assume that an unsound axiom can be generated for the function Bad above. Then we are in one of two cases:

• There is an input, allowed by Bad's precondition, for which its postcondition is violated at the end of the call. In this case, as long as the unsound axiom cannot be used to verify Bad itself, which is the case whenever Bad is not mutually recursive, the proof of Bad will reveal this error.
• The postcondition of Bad is valid for every input for which it terminates, allowing Bad to be verified completely, but there is an input allowed by Bad's precondition for which it does not terminate. For example, with the following body, the postcondition of Bad can be discharged easily:

This second case, which can also arise for axioms generated for definitions of expression functions, is not currently detected by the tool, as GNATprove assumes termination of every called subprogram. To allow easier inspection of GNATprove's assumptions, we plan to record them on a user readable file.