[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