[Spark2014-discuss] Loop invariant for bubble sort

Hugues Jérôme hugues.jerome at gmail.com
Wed Jul 2 18:32:15 CEST 2014


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 :(

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

The complete code is actually:

 procedure Sort (A : in out T_Arr) is
    Finished : Boolean;
 begin
    for I in reverse A'First + 1 .. A'Last loop
       Finished := True;

       for J in A'First .. I - 1 loop
          if A (J) > A (J + 1) then
             Finished := False;
             Swap (A, J, J + 1);
          end if;
          pragma Assert (A (J) <= A (J + 1));
          pragma Loop_Invariant
            (A (J) <= A (J + 1) and then
                 (for all K in A'First .. J => (A (K) <= A (J + 1))));
       end loop;
       pragma Assert (A (I - 1) <= A (I));
       pragma Assert
         (A (I - 1) <= A (I) and then -- proved
            (for all K in I .. A'Last => A (K - 1) <= A (K)));

       exit when Finished;

    end loop;
 end Sort;

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? 

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

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

--
Jérôme Hugues, ISAE/DMIA
Jerome.HUGUES at isae.fr - (+33) 5 61 33 91 84

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Hugues J?r?me.vcf
Type: text/directory
Size: 437 bytes
Desc: not available
URL: <http://lists.forge.open-do.org/pipermail/spark2014-discuss/attachments/20140702/4ebf0d10/attachment.bin>


More information about the Spark2014-discuss mailing list