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,ade418da030a5253
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!postnews.google.com!g28g2000yqh.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: Trouble cutting loops with SPARK. Advice?
Date: Sun, 7 Mar 2010 02:22:43 -0800 (PST)
Organization: http://groups.google.com
Message-ID: 
 <484e7806-9242-4c20-a057-cbc34fd67f03@g28g2000yqh.googlegroups.com>
References: <4b92bb37$0$2342$4d3efbfe@news.sover.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 1267957363 9050 127.0.0.1 (7 Mar 2010 10:22:43
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Sun, 7 Mar 2010 10:22:43 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: g28g2000yqh.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),gzip(gfe),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:9453
Date: 2010-03-07T02:22:43-08:00
List-Id: <comp.lang.ada>

Peter,

> I get the feeling there is a trick here that I'm overlooking. Is my code
> wrong? It looks okay to me. :)

Your code is OK and yes there is something that you are probably
overlooking.

It's not really a 'trick' - more an oddity of the language for proving
code in 'for' loops that have range constraints.  (Loops like that are
the one exception to the SPARK rule that there are no anonymous
subtypes.)

The problem is that the value of the variables that provide the loop
bounds (in your code the variable Characters_To_Copy) can be changed
within the loop, so any reference to Characters_To_Copy within an
assertion in the loop means the *current* value, not the value that
defined the loop bound.  The Examiner doesn't check to see whether
Characters_To_Copy is changed within the loop (it just assumes that it
might be changed), so in this case you have to state that it is
unchanged in the loop assertion.

SPARK therefore supplies a notation for the value of any variable on
entry to a loop - append % to the name - so Characters_To_Copy% within
a proof context in the loop means the value of Characters_To_Copy on
entry to the loop.

The loop assertion that works for the code in your message is:
         --# assert I >= 1
         --#  and   Characters_To_Copy <= Line'Length
         --#  and   Characters_To_Copy = Characters_To_Copy%;
placed at the beginning of the loop.

Cheers,

Phil