[Spark2014-discuss] Loop invariant for bubble sort

Claude Marche Claude.Marche at inria.fr
Wed Jul 2 22:31:08 CEST 2014

Good evening,

On 07/02/2014 06:32 PM, 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 :(

A first general remark: I think that bubble sort is not only a badly
performing sorting algorithm, but also a difficult one to prove.
One should start with selection sort.

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

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

This variant is more general, although provable from your own version,
but with an induction, hence automated provers have hard time to get it.

- Claude

More information about the Spark2014-discuss mailing list