From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,6d79efdb8dde2c5a
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!postnews.google.com!x25g2000yqj.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK : third example for Roesetta - reviewers welcome
Date: Sun, 15 Aug 2010 21:41:42 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <db998742-7289-4b74-9177-a8bbff0670be@x25g2000yqj.googlegroups.com>
References: <op.vhguffh3ule2fv@garhos>
 <589eea9a-0b14-4ae5-bf62-9abf4b33e7fb@i31g2000yqm.googlegroups.com>
 <i49oif$1c85$1@adenine.netfront.net>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
X-Trace: posting.google.com 1281933702 25032 127.0.0.1 (16 Aug 2010 04:41:42
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Mon, 16 Aug 2010 04:41:42 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: x25g2000yqj.googlegroups.com; posting-host=80.177.171.182;
 posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
 Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:13383
Date: 2010-08-15T21:41:42-07:00
List-Id: <comp.lang.ada>

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