Re: SPARK : third example for Roesetta - reviewers welcome

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

On 15 Aug, 23:09, Jeffrey Carter <spam.jrcarter....@spam.not.acm.org>
wrote:
> On 08/15/2010 11:42 AM, Phil Thornley wrote:
>
>
>
> >> * In the loop inside of Search there are Check annotations which was not
> >> strictly needed but which I still left for more expressiveness. Is that OK
> >> ? Not too much ?
> > I prefer user rules to large numbers of check annotations, but YMMV.
>
> The large number of Check annotations seems to my untrained eye an unusual way
> to use SPARK. As a comparison, the Tokeneer "core" code is 34769 LOC and
> contains 27 Check annotations, a much lower ratio of Check/LOC. Is this a good
> way to present SPARK on Rosetta?

It is certainly unusual (I worked on the proofs for a program of
150,000 lines and there was just 1 check annotation), and I agree that
it may put readers off.

I think that it is just about acceptable if it avoids creating *any*
user rules (because adding these rules to the source might also put
people off).

However it is likely that most other examples won't have this problem
- integer division (which causes the problems here) is an area where
the Simplifier needs a lot of help either by check annotations or user
rules.

If Yannick wants to keep them then perhaps he could add some comments
to the program description saying that this use of check annotations
is unusual.

Cheers,

Phil