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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,da5197b9dca0ed40
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!postnews.google.com!s9g2000yqd.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: Processing array subsections, a newbie question.
Date: Tue, 15 Jun 2010 02:45:21 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <c21481a1-4039-4fe5-bb40-822a1f691b4a@s9g2000yqd.googlegroups.com>
References: <4c13db30$0$2391$4d3efbfe@news.sover.net>
 <alpine.LRH.2.00.1006141902370.14982@64bit-RedHat-Enterprise-Linux6beta>
	<m27hm1z9jp.fsf@pushface.org> <4c16c088$0$2366$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 1276595121 3354 127.0.0.1 (15 Jun 2010 09:45:21
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Tue, 15 Jun 2010 09:45:21 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: s9g2000yqd.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)
Xref: g2news1.google.com comp.lang.ada:11749
Date: 2010-06-15T02:45:21-07:00
List-Id: <comp.lang.ada>

On 15 June, 00:54, "Peter C. Chapin" <pcc482...@gmail.com> wrote:

> 'First' and 'Last' are reserved by SPARK as FDL identifiers. Similarly 'Start'
> and 'Finish' are reserved by SPARK.

There is a well-hidden feature of the Examiner to get over this
problem - use the qualifier -fdl=your_string.
(Where your_string is not either "accept" or "reject" or any
abbreviation of these.)

It's described in Section 3.1.5 of the Examiner User Manual (the
section on command qualifiers) but is not mentioned in the section on
reserved words (5.3, where you would really expect to find it).

I only discovered this a couple of weeks ago, but the line:
-fdl=my
is now a permanent addition to my switch files.

Here is a program that examines and proves OK with that qualifier:
(For the non-SPARK readers, every identifier in this code is one of
the reserved words that would otherwise cause an error.)
(For the pedants: use of any identifier in this code is not a
recommendation to use that identifier in any other code.)

package body Sequence
is

   type Var is range 0 .. 10_000;

   procedure Pred (First : in     Var;
                   Last  : in out Var)
   --# derives Last from *, First;
   is
      Start  : Var;
      Finish : Var;
      Succ   : Var;
   begin
      Succ   := Var'First;
      Start  := First;
      Finish := Last;
      if Start < Last then
         for Element in Var range Start + 1 .. Finish loop
            Succ := Succ + 1;
            --# assert Succ <= Element - Start
            --#   and  Start >= 0;
         end loop;
      end if;
      Last := Succ;
   end Pred;

end Sequence;

Cheers,

Phil