Re: SPARK - Bubble Sort on Rosetta Code

[Simon Wright <simon@pushface.org>]

Phil Thornley <phil.jpthornley@gmail.com> writes:

> 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

It took me a while to find them -- at
http://rosettacode.org/wiki/Sorting_algorithms/Bubble_sort#SPARK.

> The first is simply shown to be type-safe.

Is this the same as "guaranteed free of any run-time error"?

What would non-SPARK code do to make it fail?

> The second, with identical Ada code, proves that the output array is
> sorted.

Are zero-length arrays forbidden in SPARK? I ask because of 

      --# check A'Last <= A'First -> A'Last = A'First;

(what's that -> ? I understood that the syntax was
   'check <boolean expression>').