Formal verification tools like GNATprove rely on two main inputs from programmers:

• subprogram contracts (preconditions and postconditions)
• loop invariants

While the first ones are easy to understand (based on the "contract" analogy, in which a subprogram and its caller have mutual obligations), the second ones are not so simple to grasp. The need is the same though: like calls are "opaque" to the formal verification tool, hence the need for contracts on subprograms, loops are also "opaque" to the formal verification tool, hence the need for loop invariants.

Note that static analysis tools on the contrary do not require either contracts or loop invariants. It is due to the difference in technology between static analysis tools and formal verification tools: the first ones do not require annotations, but they are less powerful, leading to more a posteriori manual work (the review of false positives) if one wants to use them as verification tools instead of simply bug-finding tools.

A loop invariant is a special assertion, expressed with a pragma, that is true at each iteration of the loop. It is executed as a regular assertion, but used differently from assertions by the formal verification tool. For example, here is a function Get_Prime searching for the smallest prime number between Low and High, and the loop invariant giving the range of values of J, and expressing that no integer between Low and the current value J is prime:

The loop invariant states here properties related to the loop index J: because the value of J changes during the loop, the formal verification tool knows about J only the properties that are stated in the loop invariant. On the code above, GNATprove proves the loop invariant in two stages: 

• It proves first that the loop invariant is true at the first iteration.
• It proves then that, assuming the loop invariant held at the previous iteration, it still holds at the next iteration.

This strategy looks a lot like the proof by induction that all students learn in school. Here are the two corresponding checks that GNATprove proves:

Now, loop invariants in SPARK 2014 are a bit different from the classical "Hoare" loop invariants (invented by C.A.R. Hoare in 1969), as implemented in Eiffel, JML, ACSL or Spec#.

In all these languages, the loop invariant must be true when reaching a loop, each time the loop resumes, and at loop end. If we had adopted this style of loop invariants in SPARK 2014, the code above would have to be written:

You can see immediately that the loop invariant gets more complex, because:

• Low might be greater than High, hence the guard "if Low <= High" before stating the range of J, for the loop invariant to hold when reaching the loop
• J may end up being greater than High by 1, hence the range for J "Low .. High + 1", to account for the possible highest value at loop end
• J has been increased before resuming the loop, hence the range for J from Low to J - 1, due to the fact the loop invariant is checked at the beginning of an iteration.

Hence the decision in SPARK 2014 to allow loop invariants anywhere in the loop, so that the user can put it where it is most natural to express. The loop invariant thus needs not hold when reaching the loop, if the loop is never entered, nor does it need to hold when exiting the loop.

In case you wonder if the loop invariant given previously is useful, it allows you to prove the following contract automatically with GNATprove (expressed with contract cases):