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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	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,UTF8
Path: 
 g2news1.google.com!news4.google.com!news2.google.com!npeer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post02.iad.highwinds-media.com!news.flashnewsgroups.com-b7.4zTQh5tI3A!not-for-mail
From: Stephen Leake <stephen_leake@stephe-leake.org>
Newsgroups: comp.lang.ada
Subject: Re: SPARK : third example for Roesetta - reviewers welcome
References: <op.vhguffh3ule2fv@garhos>
 	<589eea9a-0b14-4ae5-bf62-9abf4b33e7fb@i31g2000yqm.googlegroups.com>
 	<i49oif$1c85$1@adenine.netfront.net> <op.vhh3bwnwxmjfy8@garhos>
Date: Mon, 16 Aug 2010 03:50:33 -0400
Message-ID: <82mxsnuhbq.fsf@stephe-leake.org>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.1 (windows-nt)
Cancel-Lock: sha1:KdMHtDUIU49Z4H2u0oD4h07TEn0=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
X-Complaints-To: abuse@flashnewsgroups.com
Organization: FlashNewsgroups.com
X-Trace: 445494c68edb8e029e66106629
Xref: g2news1.google.com comp.lang.ada:13388
Date: 2010-08-16T03:50:33-04:00
List-Id: <comp.lang.ada>

"Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes:

> Le Mon, 16 Aug 2010 00:09:17 +0200, Jeffrey Carter
> <spam.jrcarter.not@spam.not.acm.org> a écrit:
>> 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?
> There is no Magic here, what you do not have in Check annotations, you
> hide it in user rules. The reason why I do not like it, is because you
> do  not see the proofs any more (or great part of it are missing),
> this is not  any more part of the source. Proofs should come with the
> implementation. I  cannot dissociate both.
>
> May be a matter if personality also.
>
>> Is this a good way to present SPARK on Rosetta?
> Rightly, at this place, this is moreover a special case: better to
> show what annotations are than to hide it. People aware of SPARK may
> guess  implicit parts... other users will not. So better show it
> explicitly (as  long as the target is to explain what formal
> validation means with  interpretable examples).
>
> At least, I feel it this way. Tell about your comments.

The user rules are part of the SPARK source. The file names may not end
in .ad?, but they are still source. 

Is there a way to get the Rosetta website to make that clear?

-- 
-- Stephe