For all the power that comes with proof technology, one sometimes has to pay the price of writing a loop invariant. Along the years, we've strived to facilitate writing loop invariants by designing a methodology in four easy steps for writing a loop invariant, by providing loop patterns and their corresponding loop invariants, by generating automatically the part of loop invariants that talks about unmodified parts of objects, but writing loops invariants remains difficult sometimes, in particular for beginners.

At the same time, some loops look so simple that they don't seem to require a loop invariant. Take for example the following loop that initializes an array, with value J at index J for every index:

Suppose you want to prove that indeed Init ensures that A(J) is equal to J at every index J:

Previously, you would have needed a loop invariant for GNATprove to be able to prove this postcondition. This is not needed anymore. Instead, GNATprove unrolls the loop in Init as if it were defined as:

This allows GNATprove to prove the postcondition without loop invariant.

Not every loop can be unrolled this way. Firstly, we need to know how many times the loop should be unrolled, so it's not possible to unroll while-loops, plain-loops, or for-loops that have bounds not known at compile time. Secondly, we don't want to unroll loops that have thousands of iterations, or it would lead to an explosion in complexity that would defy the purpose of this feature. Hence we limit unrolling to loops with less than 20 iterations.

Finally, we want to give the user control over this feature, so we do not unroll loops which contain already a loop invariant (or a loop variant), which is a sign that the user wants to use here the usual proof mechanism.

This new feature in SPARK has proved very effective on the first examples we've tried it. For example, it allowed to prove a Tic-Tac-Toe implementation by my colleague Quentin Ochem (for a student training course) without loop invariants, instead of the 16 loop invariants that were originally needed. I also tried it on the computation of the longest common prefix from two starting points in a text, a typical beginner example in SPARK. The original code uses a maximal length of 100000 for the text array, and a while-loop to move forward in the array. Just replace that with a maximal length of 10 and a for-loop, and you get an automatic proof of the rich postcondition of this function without any loop invariant! Transforming a while-loop into a for-loop is not that hard, provided you have a higher bound N on the number of iterations. The while-loop:

becomes:

Similarly, on another archetypal learning example, binary search, one can change the while-loop "while Left <= Right loop" into a simple for-loop "for J in U'Range loop" as control will exit as soon as the array is found to be ordered. Again, GNATprove manages to prove the rich postcondition of binary search without a loop invariant in that case.

Besides its interest for beginners, loop unrolling could also be convenient to explore new algorithms, as a way to get confidence in the implementation on a small scale before moving to the final production-level scale. Not only the provers can be relied on to prove for-loops with low number of iterations (under 20), but counterexamples also tend to be better on the unrolled loops, so interaction with the tool is twice improved.

That feature does not eliminate the need for loop invariants in the general case, but it makes it easier to learn and to experiment with SPARK, before the need for loop invariants pushes one to learn how to write them. To know more about this feature, see the SPARK User's Guide.