Re: SPARK - Bubble Sort on Rosetta Code

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

On 26 Aug, 23:32, Simon Wright <si...@pushface.org> wrote:
> Phil Thornley <phil.jpthorn...@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.
Ooops, sorry about not including that.

> > The first is simply shown to be type-safe.
>
> Is this the same as "guaranteed free of any run-time error"?
Yes - the Wikipedia page on type safety (http://en.wikipedia.org/wiki/
Type_safety) says "In the context of static (compile-time) type
systems, type safety usually involves (among other things) a guarantee
that the eventual value of any expression will be a legitimate member
of that expression's static type."

I've always wanted a shorter phrase than "proof of absence of run-time
error" and Rod used the phrase type-safe in his recent announcement
about SPARKSkein.

> What would non-SPARK code do to make it fail?
Get one of the bounds on the inner loop wrong?  Get the termination
condition wrong for the outer loop and increment the pointer past the
end?

> > The second, with identical Ada code, proves that the output array is
> > sorted.
>
> Are zero-length arrays forbidden in SPARK?
Yes - any array must use a named index subtype, and null subtype
ranges are forbidden (which can be checked by the Examiner because the
bounds of subtype ranges must be static).

>                                        ... I ask because of
>
>       --# check A'Last <= A'First -> A'Last = A'First;
That's an example of a 'tactical' check annotation that helps with
proing some of the VCs. (It converts a potential path into an
infeasible one, which makes it a lot easier to prove the post-
condition.)

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

Cheers,

Phil