[Spark2014-discuss] Loop invariant for bubble sort

Yannick Moy moy at adacore.com
Wed Jul 2 23:33:10 CEST 2014

-- Hugues Jérôme (2014-07-02)
> Hi,
> I’m trying to prove a bubble sort, and face some issues on invariants (an area where I need some more insights than I expected). I took for granted from Claire on her last blog post that proving a sort being correct was “easy", and tried, but failed :(

Hi Jérôme,

The blog post says that proving sorting is "easier" than proving that the result is a permutation of the input, but not that it's "easy". So don't feel bad! :)

> Let me explain where I’m stuck (complete code is there: https://github.com/yoogx/spark_examples/tree/master/sparkle )
> The problem is not the implementation of the sort itself, it may eventually be wrong (yet worked on a few tests, so I’m somewhat confident). My problem is on the analysis of the error messages and their interpretation towards a correct loop invariant 
> Here is where it starts;
> for I in reverse A'First + 1 .. A'Last loop
> [..]      
>       pragma Assert (A (I - 1) <= A (I));
>       pragma Loop_Invariant
>         (A (I - 1) <= A (I) and then -- proved
>            (for all K in I .. A'Last => A (K - 1) <= A (K)));
> GNATProve accepts to discharge the assert, and the first part of the loop invariant.
> It refuses to discharge the second part, and returns
> spark-bubble_sort.adb:46:44: warning: loop invariant might fail after first iteration, requires A (K - 1) <= A (K)
> OK, but if the first part of the invariant is proved, shouldn’t the tool infer the second part? This bugs me

No, this is not sufficient. The assertion 
    pragma Assert (A (I - 1) <= A (I));
simply restates what the tool knows from the loop invariant of the inner loop: the new value that has been put in A(I) is greater than previous values (and in particular A(I-1)).

But what you need to prove is that:
1) assuming only the loop invariant (so here: the array is sorted in increasing order from I-1 to A'Last)
2) ignoring everything else about variables modified in the loop (so here: we don't know anything about values of A between A'First and I-2)
3) executing the end of the loop (just the exit here), the test of the loop, continuing in those cases it does not exit, and the start of the loop (just the inner loop here), show that the loop invariant still holds

You can see that step (2) above does not allow proving the loop invariant in step (3). If you assume any value can be in the first part of the array A, then there is no way you can show that such a value when copied to index I is less than the value at index I+1.

Also, you need to know that the inner loop does not modify elements of the array after index I.

I attach a patch on Sort that allows to prove it completely in a few minutes, with a timeout of 120s and the proof strategy "progressively split", so using:

$ gnatprove -Pspark.gpr --timeout=120 --proof=progressive --limit-subp=spark-bubble_sort.ads:17

Note that I commented out the early exit when Finished is True. If you want to uncomment it and still prove the postcondition of Sort, you'll need to add new a loop invariant for the inner loop, that state that Finished remains True while the start of the array is sorted.

> GNATProve reports that because of the “guilty statement”, he has a counter example. But then why is the assert before discharged, as well as the first part of the invariant? 

Currently, GNATprove does not report counter-examples (although we're working on that), only traces that correspond to the path on which a check is not proved. But if you give too small a timeout, you'll still get these traces for the first path through the subprogram on which the prover does not answer "yes" in the given time! (provided you use the "proof by path" or "progressively split" proof strategy)

See for example the snapshot attached produced with SPARK GPL 2014 on the provable code, but this time using a short timeout of 1s.

> On a side note: with GPL 2014 toolset, the output in GPS is strange, I have a “magnify” icon on a line whose content is a duplicate of the line below, in place of the actual error message from GNATProve for line 46. Just try to prove the file with the per path strategy

I don't see this, look at the snapshot attached. Can you send a snapshot or a reproducer?

> Thanks for bringing some lights, I’m quite lost for now

As I said during the SPARK 2014 tutorial at Ada Europe last week, loop invariants are the heart of darkness of deductive methods! But there is nothing magic, once you understand how they work.

Hope that helps.
Yannick Moy, Senior Software Engineer, AdaCore

-------------- next part --------------
A non-text attachment was scrubbed...
Name: sort.patch
Type: application/octet-stream
Size: 1740 bytes
Desc: not available
URL: <http://lists.forge.open-do.org/pipermail/spark2014-discuss/attachments/20140702/482b89f8/attachment-0001.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: sort.png
Type: image/png
Size: 950825 bytes
Desc: not available
URL: <http://lists.forge.open-do.org/pipermail/spark2014-discuss/attachments/20140702/482b89f8/attachment-0001.png>
-------------- next part --------------

More information about the Spark2014-discuss mailing list