SPARK - Bubble Sort on Rosetta Code

[Phil Thornley <phil.jpthornley@gmail.com>]

I've put some SPARK code for the Bubble Sort task on Rosetta Code and
I would welcome opinions on whether they make a good showcase for
SPARK

I've used the Ada version on there as the starting point, with Integer
for the stored element and for the array index,

There are three versions:

The first is simply shown to be type-safe.

The second, with identical Ada code, proves that the output array is
sorted. This requires just two simple proof rules as the inner loop
scans the complete array for every pass of the outer loop.

The third version scans a reducing portion of the array in the inner
loop and this makes the proof quite a bit more complex. My main
concern is that the number of proof rules that this requires could
look rather frightening to a casual browser and do more harm than
good.

Cheers,

Phil