[Spark2014-discuss] Loop invariant for bubble sort

John McCormick mccormick at cs.uni.edu
Wed Jul 2 21:36:16 CEST 2014


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.

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.forge.open-do.org/pipermail/spark2014-discuss/attachments/20140702/661779af/attachment.html>


More information about the Spark2014-discuss mailing list