Re: SPARK : third example for Roesetta - reviewers welcome

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

On 15 Aug, 23:19, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> Le Sun, 15 Aug 2010 22:57:21 +0200, Yannick Duchêne (Hibou57)  
> <yannick_duch...@yahoo.fr> a écrit:> I saw something wrong in this version.
>
> Half false alarm, half True alarm: there is not way to have an empty array  
> in SPARK. But I don't really enjoy the lack of a test for the empty array  
> case, as a SPARK program is always a valid Ada program, and may be  
> compiled ignoring any SPARK error as well. This is perfectly possible to  
> compile this passing Search an empty array. I would prefer SPARK allow  
> empty array, and thus end into the creation of more robust units.
>
> So whatever SPARK says about it, I will get back the test for the empty  
> array case.

But if you put that test back in you are going to get flow errors for
the added path - because Position will be exported but no value will
be assigned to it.

There's an interesting general point here - the 'SPARK' assumption is
that the complete program is SPARK, so an empty array can't happen (it
would require a index subtype with 'First > 'Last, which is a semantic
error).

However, if we start to see individual packages being put into the
public domain then the calling program could well be just Ada, so an
empty array becomes a possibility.

My personal view is against changing the code of SPARK operations to
handle non-SPARK constructs, because it will cause all sorts of
problems (like the flow error in this case).

For the examples in Rosetta Code we should just state that assumption
in the accompanying text, since these code samples are for
demonstrating language features rather than providing a source code
library.

But there is still a problem in the real world. Perhaps what is needed
is an 'Ada to SPARK' interface to check for violations.  One
possiblity would be for the SPARK operation to become internal to the
package and the body of the visible operation to check that the array
is non-null and only call the internal operation if it's OK (the code
of that operation will probably have to be hidden from the Examiner).

Cheers,

Phil