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: a07f3367d7,b49755ab898bcffd
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news2.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 again : for-loop vs single loop - a strange case
Date: Fri, 28 May 2010 01:21:27 +0200
Organization: Ada At Home
Message-ID: <op.vdd0h1kuule2fv@garhos>
References: <op.vddp3fvvxmjfy8@garhos>
 <40qtv5pfcsomupgedmd5iait1bnbtmdlg8@4ax.com>
NNTP-Posting-Host: XlijgeMd1lHVMWRsQUf7bg.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.53 (Win32)
Xref: g2news2.google.com comp.lang.ada:12101
Date: 2010-05-28T01:21:27+02:00
List-Id: <comp.lang.ada>

Le Thu, 27 May 2010 23:50:06 +0200, Brian Drummond  =

<brian_drummond@btconnect.com> a =C3=A9crit:
Hi Brian,

> Is it relevant here that the range of L is known in the first loop, an=
d
> can (presumably) be shown to be less than T'Size?
>
> Perhaps L in the second example can be declared of a subtype with
> appropriate range? (If it already is, that wasn't shown in the posted
> code)
Yes, sorry, I forget it. In the simple loop case, L is of the same type,=
  =

that is, it is declared as of type T and T'First is equal to 1. So the  =

declaration of L in the for-loop and the declaration of L with the simpl=
e  =

loop, are the same. N is obviously of type T too.

What puzzles me, is that the expression in the Check clause, does not  =

depend on any context, it is purely mathematical, thus it should be as  =

provable with the simple loop as it is with the for-loop.

I've just done a test a few seconds ago. If I copy the same Check clause=
  =

between the =E2=80=9CL :=3D 1;=E2=80=9D statement and the begin of the l=
oop, that is:


    L :=3D 1;

    --# check (2 ** (T'Pos (L) + 1)) =3D ((2 ** T'Pos (L)) * 2);

    loop
       ...
       --# assert ...;
       ...
       --# check (2 ** (T'Pos (L) + 1)) =3D ((2 ** T'Pos (L)) * 2);
       exit when L =3D Length;
       L :=3D L + 1;
       ...
    end loop;

then the first occurrence of the Check, at the first location, is proved=
  =

right away by the simplifier, and the second occurrence, is still not  =

proved.

Really funny, as the expression does not depends on any context and all =
 =

numbers/expression which appears in, are Universal_Integer [ARM 2005 Ann=
ex  =

K (175)], so there should be no matter about any range of any kind. Note=
:  =

T'Last is small, it is actually 8.

Will try some others things later. I believe this is an interesting topi=
c  =

(unless I did a gentle clumsy thing which I have not already figured).

Have a nice day/night.

-- =

There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.