SPARK - Bubble Sort on Rosetta Code

SPARK - Bubble Sort on Rosetta Code

[Phil Thornley]

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

I've used the Ada version on there as the starting point, with Integer
for the stored element and for the array index,

There are three versions:

The first is simply shown to be type-safe.

The second, with identical Ada code, proves that the output array is
sorted. This requires just two simple proof rules as the inner loop
scans the complete array for every pass of the outer loop.

The third version scans a reducing portion of the array in the inner
loop and this makes the proof quite a bit more complex. My main
concern is that the number of proof rules that this requires could
look rather frightening to a casual browser and do more harm than
good.

Cheers,

Phil

Re: SPARK - Bubble Sort on Rosetta Code

[Yannick Duchêne (Hibou57)]

Le Thu, 26 Aug 2010 11:18:20 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:

> 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
Personal opinion: I still do not feel user rules are nice (and this case  
confirms my opinion to me).
But in the large, I agree, except with the length and the weight of user  
rules of the last examples compared to the source.

Just a tiny detail and a less tiny
“--# derives A from A;” may be clearer than “--# derives A from *;”
May be nice to say there are two level of usage of SPARK: proof of  
semantic and proof of runtime-error free. It is implicit in the first case  
(as it talks about free of runtime error), but this may be nice to tell  
about it explicitly.

May be this would be better to state this in the page you created about  
the proof process.

In the page The SPARK Proof Process

“The verification conditions generated depend on the annotations that have  
been specified in the SPARK source and the properties that they specify.”.

This miss to tell about validation condition created based on the type  
system. This does not requires annotations.

“This normally proves 95-99% of all verification conditions.”

This is more likely to be true only when only free-of-runtime-error is a  
concern. The distinction should be made here.

I like what you did for the bubble sort, but I am really afraid when I  
compare the length of the whole SPARK example to the others. May be the  
one with the Sorted postcondition would be enough. And indeed, this single  
one would make the SPARK example not much longer than the Ada one. Well,  
after all, both the one with the sorted postcondition and the one with  
free of runtime error only. Just feel this would be nice to state the  
first one is not strictly less complete than the second one in some  
regards, just that the target is not the same.

Here are, this was my feelings.

Have a nice day

-- 
* 3 lines of concise statements is readable, 10 pages of concise  
statements is unreadable ;
* 3 lines of verbose statements may looks unuseful, 10 pages of verbose  
statements will never looks too much pedantic

Re: SPARK - Bubble Sort on Rosetta Code

[Simon Wright]

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>').

Re: SPARK - Bubble Sort on Rosetta Code

[Yannick Duchêne (Hibou57)]

Le Fri, 27 Aug 2010 00:32:08 +0200, Simon Wright <simon@pushface.org> a  
écrit:
> (what's that -> ? I understood that the syntax was
>    'check <boolean expression>').
The Implies operator of Boolean logic


-- 
* 3 lines of concise statements is readable, 10 pages of concise  
statements is unreadable ;
* 3 lines of verbose statements may looks unuseful, 10 pages of verbose  
statements will never looks too much pedantic

Re: SPARK - Bubble Sort on Rosetta Code

[Yannick Duchêne (Hibou57)]

Le Thu, 26 Aug 2010 23:40:04 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> I like what you did for the bubble sort, but I am really afraid when I  
> compare the length of the whole SPARK example to the others.
May I finally express my real though about the length topoc (hope it gonna  
not be miss-interpreted) : I was afraid this may look a bit spammy  
compared to others (but may be this is just a silly feeling of mine).  
Well, at least this show how SPARK is special ;)


-- 
* 3 lines of concise statements is readable, 10 pages of concise  
statements is unreadable ;
* 3 lines of verbose statements may looks unuseful, 10 pages of verbose  
statements will never looks too much pedantic

Re: SPARK - Bubble Sort on Rosetta Code

[Phil Thornley]

On 26 Aug, 22:40, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> Le Thu, 26 Aug 2010 11:18:20 +0200, Phil Thornley  
> <phil.jpthorn...@gmail.com> a écrit:
>
> > 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
>
> Personal opinion: I still do not feel user rules are nice (and this case  
> confirms my opinion to me).
> But in the large, I agree, except with the length and the weight of user  
> rules of the last examples compared to the source.
But of the 11 rules for the last example, only two of them do not
involve a proof function reference.  If you have proof functions then
you have to have proof rules for them.

> Just a tiny detail and a less tiny
> “--# derives A from A;” may be clearer than “--# derives A from *;”
My style is always to use '*' for self-dependency to give it a strong
visual emphasis. Self-dependency is different as it can be created by
the absence of code, whereas all other dependencies require the
presence of code.

> May be nice to say there are two level of usage of SPARK: proof of  
> semantic and proof of runtime-error free. It is implicit in the first case  
> (as it talks about free of runtime error), but this may be nice to tell  
> about it explicitly.
That is essentially covered in the (fairly brief) description of SPARK
in it's language page.

> May be this would be better to state this in the page you created about  
> the proof process.
>
> In the page The SPARK Proof Process
>
> “The verification conditions generated depend on the annotations that have  
> been specified in the SPARK source and the properties that they specify.”.
>
> This miss to tell about validation condition created based on the type  
> system. This does not requires annotations.
>
> “This normally proves 95-99% of all verification conditions.”
>
> This is more likely to be true only when only free-of-runtime-error is a  
> concern. The distinction should be made here.
I can see a couple of improvements to the wording here, so I'll think
about these suggestions as well.

Thanks,

Phil

Re: SPARK - Bubble Sort on Rosetta Code

[Phil Thornley]

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

Re: SPARK - Bubble Sort on Rosetta Code

[Yannick Duchêne (Hibou57)]

Le Fri, 27 Aug 2010 09:35:51 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
> But of the 11 rules for the last example, only two of them do not
> involve a proof function reference.  If you have proof functions then
> you have to have proof rules for them.
Right

What about a comment to tell about ? Something like a separator line and a  
“the comings are requirement for the aboves”.
If know this may look pedantic, but I feel this may really help.

>> “--# derives A from A;” may be clearer than “--# derives A from *;”
> My style is always to use '*' for self-dependency to give it a strong
> visual emphasis.
I should not have made this comment, was not important


In
    --# assert I% = I

Why not add a tiny comment which explains I% stands for the previous value  
of I ? Annotations language of SPARK is well designed in the large, and  
mostly readable as-is without the need of comments to explain it. Except I  
feel for this kind of notation which are not intuitive. I'm pretty sure it  
is difficult to guess the meaning of the "%" here (moreover if you think  
about the C's modulo operator which this "%" inevitably recalls).


-- 
* 3 lines of concise statements is readable, 10 pages of concise  
statements is unreadable ;
* 3 lines of verbose statements may looks unuseful, 10 pages of verbose  
statements will never looks too much pedantic

Re: SPARK - Bubble Sort on Rosetta Code

[Phil Thornley]

On 27 Aug, 08:57, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> On 26 Aug, 23:32, Simon Wright <si...@pushface.org> wrote:> Phil Thornley <phil.jpthorn...@gmail.com> writes:
> >                                        ... 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.)

I thought about that a bit more and realised that it isn't necessary.
(Must have got left there from an earlier version of the code.)

So I've removed it from both of the versions it appeared in.

Cheers,

Phil

Re: SPARK - Bubble Sort on Rosetta Code

[sjw]

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

Re: SPARK - Bubble Sort on Rosetta Code

[Phil Thornley]

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