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.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no 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,ASCII
Path: 
 g2news2.google.com!news2.google.com!Xl.tags.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!nntp.bt.com!news.bt.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 27 May 2010 16:44:30 -0500
From: Brian Drummond <brian_drummond@btconnect.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK again : for-loop vs single loop - a strange case
Date: Thu, 27 May 2010 22:50:06 +0100
Reply-To: brian@shapes.demon.co.uk
Message-ID: <40qtv5pfcsomupgedmd5iait1bnbtmdlg8@4ax.com>
References: <op.vddp3fvvxmjfy8@garhos>
X-Newsreader: Forte Agent 1.7/32.534
MIME-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Usenet-Provider: http://www.giganews.com
X-AuthenticatedUsername: NoAuthUser
X-Trace: 
 sv3-Z3x6ktj6+7GP0Tx6+Uhm7rWhlmkU/uN270lN8H1WqEQp7DIlq/FahbepUL8bUUoT9Swo9qSCCx6hJUp!aENViTbEVzWeMUth+wKP9N1oEOUKFJUxHfuMq9vb1XjzmUof1RUMSj43Di4KyeP99mfZnf3g1ic9!HA==
X-Complaints-To: abuse@btinternet.com
X-DMCA-Complaints-To: abuse@btinternet.com
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.40
Xref: g2news2.google.com comp.lang.ada:12099
Date: 2010-05-27T22:50:06+01:00
List-Id: <comp.lang.ada>

On Thu, 27 May 2010 21:36:41 +0200, Yannick Duch�ne (Hibou57)
<yannick_duchene@yahoo.fr> wrote:

>Hi all,
>
>This will require some further investigation on my own side, however, I  
>would like to open a topic about it, if ever someone wants to share about  
>the same matter.
>
>I was proving something built around a for-loop. Every thing was going,  
>when I've meet a trouble and decided to switch to a classic loop and an  
>exit statement and a local variable.
>
>There was a Check clause in the for-loop, which was looking like this:
>
>    for L in T range 1 .. N loop
>       ...
>       --# assert ...;
>       ...
>       --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);
>       ...
>    end loop;
>
>
>This Check clause was proved by the Simplifier without any trouble.
>
>I then switch to a class loop, looking like this:
>
>
>    L := 1;
>
>    loop
>       ...
>       --# assert ...;
>       ...
>       --# check (2 ** (T'Pos (L) + 1)) = ((2 ** T'Pos (L)) * 2);
>       exit when L = Length;
>       L := L + 1;
>       ...
>    end loop;
>
>Then, the Simplifier was not able anymore to prove this Check. I don't  
>understand, as this Check should only depends on a basic rule, a rule by  
>definition. So why the same rule is not applied when I use a classic loop  
>instead of a for-loop ?

Is it relevant here that the range of L is known in the first loop, and
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)

- Brian