Re: SPARK - Bubble Sort on Rosetta Code

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

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