SPARK 2014 Rationale: Loop Variants

by Yannick Moy – Oct 04, 2013

I presented previously loop invariants as one of the key annotations (with subprogram contracts) that users should provide for using a tool like GNATprove. What about loop variants? On the one side, they can be omitted, and on the other side, it's up to you to check termination if you do so...

I must confess I've never been a big supporter of loop variants, so I did not care much that they get included in SPARK 2014 or not. SPARK 2005 did not have them and users have never complained about it.

I did not care because:

Many loops in critical embedded software are "for" loops, for which termination is not an issue (in Ada).
For most other loops in such software ("while" loops and "plain" loops), termination can be easily checked manually.
The remaining loops require usually a complex termination argument, that is unlikely to be proved automatically by a tool.

Loop variants made it nonetheless in SPARK 2014, with a rather elegant syntax, and a slick refinement compared to similar constructs in other languages. For example, here is the loop variant that expresses that the scalar quantity J always increases hrough the loop:

pragma Loop_Variant (Increases => J);

Because J is a scalar value (an integer or an enumeration), it is bounded by the value of its type, so it cannot increase forever without failing a range check. So, by proving that J always increases through the loop, and that no run-time error occurs in the loop, one can be sure that the loop terminates normally.

In all other languages, the loop variant must always be a decreasing positive integer. We can express it this way in SPARK 2014 too, for example the above is equivalent to:

pragma Loop_Variant (Decreases => Type_Of_J'Last - J + 1);

SPARK 2014 offers the possibility to choose which direction (increasing or decreasing) is most natural, and takes care of comparing with the right bounds. Additionally, more complex loop variants can be expressed with multiple components. A countdown in hours, minutes and seconds can use the following loop variant:

pragma Loop_Variant (Decreases => Hours,
                       Decreases => Minutes,
                       Decreases => Seconds);

Here, the first component (Hours) should decrease between two consecutive iterations of the loop, or else it stays the same and the second component (Minutes) decreases, or else this one also stays the same and the last component (Seconds) decreases. And one can mix decreasing and increasing directions of variations. Nicer than the alternative:

pragma Loop_Variant (Decreases => Hours * 3600 + Minutes * 60 + Seconds);

(plus in the above, you should also check that the expression does not fail a range check or an overflow check)

So, when is it useful? The typical example is an algorithm that iterates or traverses a collection (an array or a container), and whose termination is not obvious. I found just a few days ago the following test in our testsuite where a loop variant was useful. GNATprove proved all checks and assertions on the initial (wrong) implementation of binary search:

function Search (A : Ar; I : Integer) return T with
     Pre  => (for all I1 in A'Range =>
                (for all I2 in I1 .. A'Last =>
                   A (I1) <= A (I2))),
     Post => (if Search'Result in A'Range then A (Search'Result) = I
              else (for all Index in A'Range => A (Index) /= I));
   function Search (A : Ar; I : Integer) return T is
      Left  : U;
      Right : U;
      Med   : U;
   begin
      Left  := Ar'First;
      Right := Ar'Last;
      if A (Left) > I or else A (Right) < I then
         return 0;
      end if;
      while Left <= Right loop
         pragma Loop_Invariant
           ((for all Index in A'First .. Left => A (Index) <= I)
              and then
            (for all Index in Right .. A'Last => I <= A (Index)));
         Med := Left + (Right - Left) / 2;
         if A (Med) <= I then
            Left := Med;
         elsif A (Med) >= I then
            Right := Med;
         else
            return Med;
         end if;
      end loop;
      return 0;
   end Search;

Except that I added a very simple loop variant to show that the loop terminates:

pragma Loop_Variant (Decreases => Right - Left);

and GNATprove could not prove it!

binary_search.adb:20:10: warning: loop variant might fail

for a good reason: the loop never terminates when the value searched is in the array! The update to Med is incorrect, and should be written:

if A (Med) < I then
            Left := Med + 1;
         elsif A (Med) > I then
            Right := Med - 1;
         else
            return Med;
         end if;

which (with an updated loop invariant) leads to a fully proved implementation, including the loop variant!

For more details on loop variants, see the SPARK 2014 Refence Manual.

Posted in #Language #Formal Verification #SPARK

About Yannick Moy

Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.