Re: SPARK - Bubble Sort on Rosetta Code

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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