[Spark2014-discuss] Loop invariant for bubble sort

Claude Marche Claude.Marche at inria.fr
Wed Jul 2 22:32:44 CEST 2014



On 07/02/2014 09:36 PM, John McCormick wrote:
> Hello Jérôme,
> 
> My selection sort invariants for ordering and partitioning took nearly
> an hour to prove with alt-ergo.  If you are convinced that your
> assertions are correct (tested with assertions enabled),  you might want
> to do a proof run overnight or try alternate provers. 

This is just incredible. The Why3 version of selection sort is proved in
no time by Alt-Ergo, see

http://toccata.lri.fr/gallery/selection_sort.en.html

This deserves to be investigated.

- Claude

> John
> 
> On 7/2/2014 11:32 AM, Hugues Jérôme wrote:
>> 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
>>
>>
>>
>> _______________________________________________
>> Project spark2014 discuss mailing list
>> discuss at spark2014.forge.open-do.org
>> https://lists.forge.open-do.org/cgi-bin/mailman/listinfo/spark2014-discuss
> 
> 
> 
> _______________________________________________
> Project spark2014 discuss mailing list
> discuss at spark2014.forge.open-do.org
> https://lists.forge.open-do.org/cgi-bin/mailman/listinfo/spark2014-discuss
> 


More information about the Spark2014-discuss mailing list