Re: SPARK : third example for Roesetta - reviewers welcome

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

On 15 Aug, 22:40, Jeffrey Carter <spam.jrcarter....@spam.not.acm.org>
wrote:
> On 08/15/2010 01:19 PM, Yannick Duchêne (Hibou57) wrote:
>
> > --# pre
> > --# (Source'Length = 0) or else
> > --# (for all I in Index_Type range Source'First .. Source'Last - 1
> > --# => (Source (I) <= Source (I + 1)));
> > -- The array must be either empty or sorted from lower to higher.
>
> Is this correct? Consider the case where Source'Length = 1. In that case, the
> range in the "for all" is null; does that evaluate to True? If not, then it
> needs to be
>
> Source'Length < 2 or else (for all ...)

That's the correct way of saying that the array is ordered, and it
works fine for an array of Length 1 (or less).

The translation of that expression to FDL (the language SPARK uses for
all it's proof work) will be something like:
 for_all(i_ : integer, source__first <= i_ and i_ <= source__last - 1
            -> (element(source, [i_]) <= element(source, [i_ + 1]))) .
If source__first = source__last then the LHS of the implication is
False, and the implication itself is True.

> Even if it is correct as written, it may be misleading to non-Ada readers (whom
> we want to impress on Rosetta) who might think it implies an out-of-range access.

That's why I used the proof function 'Ordered' in my version of the
code.  To the casual reader it should look OK, and when you want to
get more formal then you define Ordered as exactly that expression
above.

Cheers,

Phil