[Spark2014-discuss] Loop invariant for bubble sort
hugues.jerome at gmail.com
Thu Jul 3 17:54:00 CEST 2014
Le 2 juil. 2014 à 22:31, Claude Marche <Claude.Marche at inria.fr> a écrit :
> A first general remark: I think that bubble sort is not only a badly
> performing sorting algorithm, but also a difficult one to prove.
I concur. The choice was made after some discussion with one colleague for preparing for some class activities.
Bubble is bad, but easy to grasp. I was just curious to see how gnat prove (and I) could perform on it
> One should start with selection sort.
next on my todo list, with insertion sort I guess
> Just a guess: it might be better to write this as
> (for all K, K' in I .. A'Last => K <= K' => A (K) <= A (K')))
Indeed, I found such strategy in ACSL variant, like in
and some archive of Frama-C. Yet, it was not clear why this one makes more sense, unless one knows in more depth how deductive methods operate.
Also, for those interested, there is an attempt in Rosetta Code using SPARK (not SPARK2014)
The trick is that they add some axioms to ease discharging some VCs
More information about the Spark2014-discuss