Re: SPARK - Bubble Sort on Rosetta Code

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

On 27 Aug, 12:03, sjw <simon.j.wri...@mac.com> wrote:
> On Aug 27, 8:57 am, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
>
> > On 26 Aug, 23:32, Simon Wright <si...@pushface.org> wrote:>
> > > 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?
>
> Sorry for lack of clarity. The page says "guaranteed free of any run-
> time error when called from any other SPARK code", and I meant, how
> might *this* code fail when called from other *non-SPARK* code? (T

Ah I see what you mean.  It's really just a catch-all statement
because the array that it imports isn't guaranteed to conform to SPARK
restrictions if called from Ada code - it could be a null array.  The
Examiner unconditionally assumes that 'First of the array index type
cannot be greater than 'Last so the proofs would be unreliable in this
case.

I'm fairly sure (;-) that there won't be any run-time error if called
with a null-array, but the static analysis doesn't prove this.

Cheers,

Phil