[Spark2014-discuss] Loop invariant for bubble sort

Hugues Jérôme hugues.jerome at gmail.com
Thu Jul 3 17:47:49 CEST 2014


Dear all,

Thanks for your various messages, and Yannick for providing an almost perfect solution.

Le 2 juil. 2014 à 23:33, Yannick Moy <moy at adacore.com> a écrit :

> 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)).

I know, consider it as part of my debug session, I wanted to see how the tool behaves.

> 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.

Indeed. I did not pay attention to the Loop_Entry attribute you used. It really deserves a note in a future blog post (unless I missed it of course)

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

It did it !
For the records, here is the log for the most complex check
spark-bubble_sort.adb:53:10: info: loop invariant preservation proved(6.95s - 19461 steps)

With a Xeon(R) CPU X5650  @ 2.67GHz CPU, so I presume 120 seconds for a laptop makes sense.
(to be honest, I had to stop using my mac air for this example ;))

> 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.

I added this part. Next step it to add comment on this example and push it to github. Thanks for the hints!

>> 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)

This is one area for improvement in the report. I should have clarified this
-> statistics report time spent, on all VCs. I noticed the “might fail” message happened before the timeout. so I considered it as being failed (because of lack of hints from invariants)

It would be great to have information on whether it is a might fail by timeout or other

>> 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?

[This was discussed directly with Yannick, issue solved in dev branch]

> 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.

Yep, I think I need a deductive methods 101. Out of curiosity, I imagine Univ. Orsay has some teaching materials, probably KSU or others. Would the list be willing to compile a list of teaching materials for inclusion on spark website?





More information about the Spark2014-discuss mailing list