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,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: 103376,103b49cd5a4719fd
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news1.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!usenet-fr.net!gegeweb.org!aioe.org!not-for-mail
From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?=
 =?utf-8?Q?=29?=
 <yannick_duchene@yahoo.fr>
Newsgroups: comp.lang.ada
Subject: Re: SPARK - Bubble Sort on Rosetta Code
Date: Fri, 27 Aug 2010 10:04:00 +0200
Organization: Ada @ Home
Message-ID: <op.vh27cyzkule2fv@garhos>
References: 
 <5688938b-2047-4fef-9ea2-730abb761d07@g17g2000yqe.googlegroups.com>
 <op.vh2eg2pqule2fv@garhos>
 <fdf146c7-7500-4a2b-80c7-92fa6a7d41e0@l6g2000yqb.googlegroups.com>
NNTP-Posting-Host: v6jzHwNKwFN2JgXrtuthGg.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes
Content-Transfer-Encoding: Quoted-Printable
X-Complaints-To: abuse@aioe.org
X-Notice: Filtered by postfilter v. 0.8.2
User-Agent: Opera Mail/10.61 (Win32)
Xref: g2news1.google.com comp.lang.ada:13773
Date: 2010-08-27T10:04:00+02:00
List-Id: <comp.lang.ada>

Le Fri, 27 Aug 2010 09:35:51 +0200, Phil Thornley  =

<phil.jpthornley@gmail.com> a =C3=A9crit:
> 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  =

=E2=80=9Cthe comings are requirement for the aboves=E2=80=9D.
If know this may look pedantic, but I feel this may really help.

>> =E2=80=9C--# derives A from A;=E2=80=9D may be clearer than =E2=80=9C=
--# derives A from *;=E2=80=9D
> 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% =3D I

Why not add a tiny comment which explains I% stands for the previous val=
ue  =

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