Re: Processing array subsections, a newbie question.

[Phil Thornley <phil.jpthornley@gmail.com>]

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