Re: SPARK - Bubble Sort on Rosetta Code

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

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