[Spark2014-discuss] Loop invariant for bubble sort

Yannick Moy moy at adacore.com
Fri Jul 4 12:32:00 CEST 2014


-- Hugues Jérôme (2014-07-03)
> 
> 
> 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)

Here is the post that presents it:
http://www.spark-2014.org/entries/detail/spark-2014-rationale-pre-call-and-pre-loop-values

Note that with SPARK GPL 2014, you should always mention the inner loop name when using Loop_Entry inside an inner loop (like I did in your example), as there was a bug causing the reference to be to the outermost loop otherwise.

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

that's perfectly reasonable to wait a few seconds for the most complex proof.

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

On my laptop with Core i7 @ 2.7 GHz CPU (so 4 cores instead of 6), this should not be much longer. I can try after you update the repository with the final version for Sort. Just upgrade your laptop! ;)

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

indeed, you might get a time spent of 0.99s when the timeout is 1s, but still stopped due to the timeout. So it's not very precise.

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

yes, that's something we'll do for the next release, as we've changed the way we handle VCs anyway.

> Yep, I think I need a deductive methods 101.

We try to provide that in the User's Guide, for example:
http://docs.adacore.com/spark2014-docs/html/ug/tutorial.html
http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html#how-to-write-loop-invariants
http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html#how-to-investigate-unproved-checks
http://docs.adacore.com/spark2014-docs/html/ug/gnatprove.html#gnatprove-by-example

Let us know if you see areas that could be improved.

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

I think the most up-to-date teaching material is the one Altran/AdaCore presented at the SPARK 2014 tutorial at Ada Europe last week. We are happy to share it with those who want to teach SPARK in their Universities, just let us know.
--
Yannick Moy, Senior Software Engineer, AdaCore






More information about the Spark2014-discuss mailing list