Processing array subsections, a newbie question.

Processing array subsections, a newbie question.

[Peter C. Chapin]

This may seem like an elementary question but I'm not too proud to ask it
anyway. :)

I'm looking for the "cleanest" way to process sequential subsections of an
array. To illustrate what I mean consider

type Buffer_Type is array(Natural range <>) of Some_Type;

The choice of Natural as an index type is perhaps not perfect, but the problem
I'm talking about here remains even if a more constrained subtype is used.

Now suppose I want to write a procedure that performs an operation on a
subsection of a Buffer_Type object. Ultimately the code needs to be SPARKable
so I can't use slices (true?). Let's say I do something like

procedure Do_Something
   (Buffer : in  Buffer_Type;
    Fst    : in  Natural;
    Lst    : out Natural;
    Ok     : out Boolean);

Here 'Fst' is intended to be a valid index into Buffer where I want to start
my processing. The processing will look over some number of Buffer's
elements, but the precise number won't be known until run time. The procedure
writes into 'Lst' the highest index value that it considers. The procedure is
careful not to access the Buffer out of bounds and it also does some other
checks on the validity of the data it finds. It writes 'True' or 'False' into
Ok depending on how happy it is. Note that in real life this procedure does
other things too... but that's not important here.

I want to invoke this procedure repeatedly on a particular buffer such that
each invocation picks up where the previous invocation left off. For example

Ok        : Boolean := True;
Index_Fst : Natural := Buffer'First;
Index_Lst : Natural;
...

while Ok and Index_Fst <= Buffer'Last loop
  Do_Something(Buffer, Index_Fst, Index_Lst, Ok);
  Index_Fst := Index_Lst + 1;
end loop;

The problem with this code is that the assignment to Index_Fst inside the loop
might raise Constraint_Error if Index_Lst = Buffer'Last after Do_Something
finishes. I can work around this problem but my solutions tend to be rather
ungainly looking. Surely there must be an easy way to handle this.

Peter

Re: Processing array subsections, a newbie question.

[Yannick Duchêne (Hibou57)]

Le Sat, 12 Jun 2010 21:11:33 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> Ok        : Boolean := True;
> Index_Fst : Natural := Buffer'First;
> Index_Lst : Natural;
> ...
>
> while Ok and Index_Fst <= Buffer'Last loop
>   Do_Something(Buffer, Index_Fst, Index_Lst, Ok);
>   Index_Fst := Index_Lst + 1;
> end loop;
>
> The problem with this code is that the assignment to Index_Fst inside  
> the loop
> might raise Constraint_Error if Index_Lst = Buffer'Last after  
> Do_Something
I know this, this is a very common problem too me : I simply use an “exit  
when not Condition” before the increment. This requires a little redesign,  
like wrapping the look in a “if Condition then”.

Sometime, to have something clean from the logical point of view, you must  
have something which is “less” visually clean... or I would better say,  
less short and more explicitly handles some cases which are merged  
otherwise.

Do you think this idea is good enough ? Does it match your requirements ?

-- 
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.

Re: Processing array subsections, a newbie question.

[Yannick Duchêne (Hibou57)]

Le Sat, 12 Jun 2010 21:11:33 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> Now suppose I want to write a procedure that performs an operation on a
> subsection of a Buffer_Type object. Ultimately the code needs to be  
> SPARKable
> so I can't use slices (true?). Let's say I do something like
I was pretty sure, however, I still checked.

RavenSPARK language manual, 4.1.2, says
4.1.2 Slices
Slices are not allowed in SPARK.

Confirmed

-- 
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.

Re: Processing array subsections, a newbie question.

[Ludovic Brenta]

"Peter C. Chapin" <pcc482719@gmail.com> writes:
> Ok        : Boolean := True;
> Index_Fst : Natural := Buffer'First;
> Index_Lst : Natural;
> ...
>
> while Ok and Index_Fst <= Buffer'Last loop
>   Do_Something(Buffer, Index_Fst, Index_Lst, Ok);
>   Index_Fst := Index_Lst + 1;
> end loop;
>
> The problem with this code is that the assignment to Index_Fst inside the loop
> might raise Constraint_Error if Index_Lst = Buffer'Last after Do_Something
> finishes. I can work around this problem but my solutions tend to be rather
> ungainly looking. Surely there must be an easy way to handle this.

How about:

Ok        : Boolean := True;
Index_Fst : Natural := Buffer'First;
Index_Lst : Natural;
...
loop
   Do_Something(Buffer, Index_Fst, Index_Lst, Ok);
   exit when not Ok;
   exit when Index_Fst = Buffer'Last;
   Index_Fst := Index_Lst + 1;
end loop;

-- 
Ludovic Brenta;

Re: Processing array subsections, a newbie question.

[Gene]

On Jun 12, 4:54 pm, Ludovic Brenta <ludo...@ludovic-brenta.org> wrote:
> "Peter C. Chapin" <pcc482...@gmail.com> writes:
>
> > Ok        : Boolean := True;
> > Index_Fst : Natural := Buffer'First;
> > Index_Lst : Natural;
> > ...
>
> > while Ok and Index_Fst <= Buffer'Last loop
> >   Do_Something(Buffer, Index_Fst, Index_Lst, Ok);
> >   Index_Fst := Index_Lst + 1;
> > end loop;
>
> > The problem with this code is that the assignment to Index_Fst inside the loop
> > might raise Constraint_Error if Index_Lst = Buffer'Last after Do_Something
> > finishes. I can work around this problem but my solutions tend to be rather
> > ungainly looking. Surely there must be an easy way to handle this.
>
> How about:
>
> Ok        : Boolean := True;
> Index_Fst : Natural := Buffer'First;
> Index_Lst : Natural;
> ...
> loop
>    Do_Something(Buffer, Index_Fst, Index_Lst, Ok);
>    exit when not Ok;
>    exit when Index_Fst = Buffer'Last;
>    Index_Fst := Index_Lst + 1;
> end loop;

Yes!  Or save a line with

loop
   Do_Something(Buffer, Index_Fst, Index_Lst, Ok);
   exit when not Ok or Index_Fst = Buffer'Last;
   Index_Fst := Index_Lst + 1;
end loop;

Loop exit (with optional naming, which obviates the problems of
'break' in C and its successors) is one of the small beauties of Ada
and an example of the way things should have been - with benefit of
hindsight - in all ALGOL-like languages.  Rather than while ... and
do ... while ... , which are inherently limited in expressive power,
every language ought to offer loop ... exit ...  end; Lord knows it
would make teaching beginning programming easier.  My favorite example
is

loop
  Put(prompt to user);
  Get(user input);
  exit when user input is okay;
  Put(the input was not correct because...);
end loop;

rather than the more complex, ugly, and potentially less efficient

declare
  Boolean Input_Okay = False;
begin
  while not Input_Okay loop
    Put(prompt to user);
    Get(user input);
    Input_Okay := test for user input is okay;
    if not Input_Okay then
      Put(the input was not correct because...);
    end if;
  end while;
end;

And my experience is that a language construct that is good for
beginning programmers is always good for general practice.

Re: Processing array subsections, a newbie question.

[Niklas Holsti]

Ludovic Brenta wrote:
> "Peter C. Chapin" <pcc482719@gmail.com> writes:
>> Ok        : Boolean := True;
>> Index_Fst : Natural := Buffer'First;
>> Index_Lst : Natural;
>> ...
>>
>> while Ok and Index_Fst <= Buffer'Last loop
>>   Do_Something(Buffer, Index_Fst, Index_Lst, Ok);
>>   Index_Fst := Index_Lst + 1;
>> end loop;
>>
>> The problem with this code is that the assignment to Index_Fst inside the loop
>> might raise Constraint_Error if Index_Lst = Buffer'Last after Do_Something
>> finishes. I can work around this problem but my solutions tend to be rather
>> ungainly looking. Surely there must be an easy way to handle this.

Constraint_Error would be raised only if Index_Lst = Natural'Last after 
Do_Something. By subtyping the index type of Buffer you could ensure 
that Buffer'Last < Natural'Last, which would avoid the risk of 
Constraint_Error. (Perhaps this is the ungainly work-around that you 
mention.)

> How about:

A few nitpicks on Ludovic's suggestion:

> Ok        : Boolean := True;

The initial value for Ok is unneccessary, as Do_Something will assign Ok 
before it it used.

> Index_Fst : Natural := Buffer'First;
> Index_Lst : Natural;
> ...
> loop
>    Do_Something(Buffer, Index_Fst, Index_Lst, Ok);

In this call of Do_Something, Index_Fst may not be a valid index for 
Buffer, since there is no preceding check that Index_Fst <= Buffer'Last, 
as there was in the original while-loop. But perhaps it is known, in the 
original context, that Buffer is not empty.

>    exit when not Ok;
>    exit when Index_Fst = Buffer'Last;

For robustness I would write Index_Fst >= Buffer'Last. (Perhaps this 
could also help some SPARK range analysis.)

>    Index_Fst := Index_Lst + 1;
> end loop;

So my suggestion is:

Ok        : Boolean;
Index_Fst : Natural := Buffer'First;
Index_Lst : Natural;
...

if Index_Fst <= Buffer'Last then
    -- Buffer is not empty, something to be done.
    loop
       Do_Something(Buffer, Index_Fst, Index_Lst, Ok);
       exit when not Ok;
       exit when Index_Fst >= Buffer'Last;
       Index_Fst := Index_Lst + 1;
    end loop;
else
    -- Buffer is empty.
    ...
end if;

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Processing array subsections, a newbie question.

[Jeffrey R. Carter]

Niklas Holsti wrote:
> 
> if Index_Fst <= Buffer'Last then
>    -- Buffer is not empty, something to be done.
>    loop

OK, we get here with Index_Fst < Buffer'Last.

>       Do_Something(Buffer, Index_Fst, Index_Lst, Ok);

And Do_Something set Ok to True.

>       exit when not Ok;

Do_Something doesn't change Index_Fst, so we get past

>       exit when Index_Fst >= Buffer'Last;

to here. Now the OP's concern, IIUC, is that Index_Lst, which Do_Something sets, 
might be = Buffer'Last = Natural'Last (seems unlikely, but I suspect this is 
simplified from an example in which the index range is more constrained and 
Index_Lst is more likely to be = Index_Subtype'Last). In that case

>       Index_Fst := Index_Lst + 1;

will raise an exception.

So it looks to me as if the correct test is

exit when Index_Lst [>]= Buffer'Last;

(Maybe Brenta meant this, and mistyped it; the variable names are very similar. 
Using _First and _Last might make such an error more obvious.)

-- 
Jeff Carter
"Why don't you bore a hole in yourself and let the sap run out?"
Horse Feathers
49

Re: Processing array subsections, a newbie question.

[Stephen Leake]

"Peter C. Chapin" <pcc482719@gmail.com> writes:

> procedure Do_Something
>    (Buffer : in  Buffer_Type;
>     Fst    : in  Natural;
>     Lst    : out Natural;
>     Ok     : out Boolean);

Change this to:

procedure Do_Something
   (Buffer : in     Buffer_Type;
    Last   : in out Natural;
    Ok     :    out Boolean);

--  Operate on Buffer (Last + 1 ..), update Last to last item operated
--  on.

-- 
-- Stephe

Re: Processing array subsections, a newbie question.

[Simon Wright]

Stephen Leake <stephen_leake@stephe-leake.org> writes:

> "Peter C. Chapin" <pcc482719@gmail.com> writes:
>
>> procedure Do_Something
>>    (Buffer : in  Buffer_Type;
>>     Fst    : in  Natural;
>>     Lst    : out Natural;
>>     Ok     : out Boolean);
>
> Change this to:
>
> procedure Do_Something
>    (Buffer : in     Buffer_Type;
>     Last   : in out Natural;
>     Ok     :    out Boolean);
>
> --  Operate on Buffer (Last + 1 ..), update Last to last item operated
> --  on.

What would happen if Buffer'First was Natural'First?

Re: Processing array subsections, a newbie question.

[Peter C. Chapin]

Gene wrote:

> Yes!  Or save a line with
> 
> loop
>    Do_Something(Buffer, Index_Fst, Index_Lst, Ok);
>    exit when not Ok or Index_Fst = Buffer'Last;
>    Index_Fst := Index_Lst + 1;
> end loop;
> 
> Loop exit (with optional naming, which obviates the problems of
> 'break' in C and its successors) is one of the small beauties of Ada...

Thanks for the suggestion (by you and others) for using a loop exit. SPARK has
some restrictions on how 'exit' can be used; I'm not sure if they will apply
to my case or not, but I can look into it. In my case there is also a state
machine involved and the exiting would have to take place inside a case
statement inside the loop. I seem to recall that SPARK has an issue with
exiting from nested control structures but I can experiment.

Peter

Re: Processing array subsections, a newbie question.

[Peter C. Chapin]

Niklas Holsti wrote:

> Constraint_Error would be raised only if Index_Lst = Natural'Last after 
> Do_Something. By subtyping the index type of Buffer you could ensure 
> that Buffer'Last < Natural'Last, which would avoid the risk of 
> Constraint_Error. (Perhaps this is the ungainly work-around that you 
> mention.)

In fact that is exactly what I'm doing now. I'm not sure if "ungainly" is the
right word to use but my concern is that now I'm using a variable to index
the array that has a subtype that can, in principle, extend outside of the
array. I haven't yet tried to prove my program free of run time errors using
SPARK but I anticipate that doing so will be harder than it might otherwise
be because of this situation. My experience with SPARK so far is that it is
very desirable to express precise intentions with one's subtypes.

On the other hand the code fragment I showed before won't prove at all, of
course, since it could in fact raise Constraint_Error. The early loop exit
approach might be workable for me. I didn't really think of that. I might
have to reorganize a few things, but I'm used to that!

Thanks for the suggestion.

Peter

Re: Processing array subsections, a newbie question.

[Yannick Duchêne (Hibou57)]

Le Sun, 13 Jun 2010 16:01:20 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
> I seem to recall that SPARK has an issue with
> exiting from nested control structures but I can experiment.
>
> Peter
You have to exit from one to an outer one. Ex. if Loop1 includes Loop2  
which includes Loop3, you cannot “exit Loop1” from Loop3 (will look for  
the reference if needed).


-- 
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.

Re: Processing array subsections, a newbie question.

[Phil Thornley]

On 13 June, 15:01, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
[...]
> Thanks for the suggestion (by you and others) for using a loop exit. SPARK has
> some restrictions on how 'exit' can be used; I'm not sure if they will apply
> to my case or not, but I can look into it. In my case there is also a state
> machine involved and the exiting would have to take place inside a case
> statement inside the loop. I seem to recall that SPARK has an issue with
> exiting from nested control structures but I can experiment.

I don't think the state machine will make any difference, but you
certainly can't exit an enclosing loop when in a case arm - you have
to move the exit(s) to after the 'end case'.

This is not usually too much of a problem, but in your code it forces
the exit to come after the increment (assuming that this has to stay
in the case arm).

As you suggest elsewhere in this thread, it is a good idea to have
subtype constraints as tight as possible.  In the situation you
describe I would define a type (to replace your use of Natural) that
has one extra value at the end (for the Index_Fst variable).  Then
define the array index as a subtype that excludes that extra value.
This should allow the increment to stay in the case arm, with the exit
following after the case.

(BTW, if you haven't tried it yet, you will find that using
unconstrained arrays creates additional work when doing run-time
checks as the VCs generated by any reference to an array element use
the limits for that array object, not just the array index subtype).

Cheers,

Phil

Re: Processing array subsections, a newbie question.

[Yannick Duchêne (Hibou57)]

Le Sun, 13 Jun 2010 18:57:14 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
> In the situation you
> describe I would define a type (to replace your use of Natural) that
> has one extra value at the end
I see what you mean, but ...
Personal feeling: this looks like a trick, would not recommend it. To be  
short: types should not defined this way. Implementation should be  
adjusted to specification (a type is a part of a specification) and not  
the opposite, that is, to adapt specifications (types here) to an  
implementation.

-- 
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.

Re: Processing array subsections, a newbie question.

[Peter C. Chapin]

Phil Thornley wrote:

> I don't think the state machine will make any difference, but you
> certainly can't exit an enclosing loop when in a case arm - you have
> to move the exit(s) to after the 'end case'.
> 
> This is not usually too much of a problem, but in your code it forces
> the exit to come after the increment (assuming that this has to stay
> in the case arm).

Yes that could be a problem for me. On the other hand *most* of the cases do
the increment. With a little thought I might be able to make them all do the
increment... and then factor that out of the case.

> As you suggest elsewhere in this thread, it is a good idea to have
> subtype constraints as tight as possible.  In the situation you
> describe I would define a type (to replace your use of Natural) that
> has one extra value at the end (for the Index_Fst variable).  Then
> define the array index as a subtype that excludes that extra value.
> This should allow the increment to stay in the case arm, with the exit
> following after the case.

That sounds like what I've got at the moment. Maybe I'll just end up sticking
with that and see how it plays out.

> (BTW, if you haven't tried it yet, you will find that using
> unconstrained arrays creates additional work when doing run-time
> checks as the VCs generated by any reference to an array element use
> the limits for that array object, not just the array index subtype).

I'll keep that in mind. I could probably defined a constrained array type
instead. In my situation the array sizes should only vary between about 20
and 40 elements. I could probably just define the array to have 40 elements
(or whatever I actually need... I'll have to check). My state machine just
returns once it is satisfied so it will ignore the extra "junk" if there is
any. I think that would be okay.

Thanks for your input.

Peter

Re: Processing array subsections, a newbie question.

[Phil Thornley]

On 13 June, 19:39, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Le Sun, 13 Jun 2010 18:57:14 +0200, Phil Thornley  
> <phil.jpthorn...@gmail.com> a écrit:> In the situation you
> > describe I would define a type (to replace your use of Natural) that
> > has one extra value at the end
>
> I see what you mean, but ...
> Personal feeling: this looks like a trick, would not recommend it. To be  
> short: types should not defined this way. Implementation should be  
> adjusted to specification (a type is a part of a specification) and not  
> the opposite, that is, to adapt specifications (types here) to an  
> implementation.
>

That's quite a severe point of view - I would classify the extra value
as a 'boundary value' as described in AQ&S 5.3.1 on subtypes.

Cheers,

Phil

Re: Processing array subsections, a newbie question.

[Stephen Leake]

Simon Wright <simon@pushface.org> writes:

> Stephen Leake <stephen_leake@stephe-leake.org> writes:
>
>> "Peter C. Chapin" <pcc482719@gmail.com> writes:
>>
>>> procedure Do_Something
>>>    (Buffer : in  Buffer_Type;
>>>     Fst    : in  Natural;
>>>     Lst    : out Natural;
>>>     Ok     : out Boolean);
>>
>> Change this to:
>>
>> procedure Do_Something
>>    (Buffer : in     Buffer_Type;
>>     Last   : in out Natural;
>>     Ok     :    out Boolean);
>>
>> --  Operate on Buffer (Last + 1 ..), update Last to last item operated
>> --  on.
>
> What would happen if Buffer'First was Natural'First?

Good point. Last should be Integer, not Natural, so Last can be
initialized to Buffer'first - 1.

Which involves defining the type with an "extra" value, which Peter said
he didn't like. I find it quite useful in situations like this.

-- 
-- Stephe

Re: Processing array subsections, a newbie question.

[Colin Paul Gloster]

On Sat, 12 Jun 2010, Peter C. Chapin sent:
|------------------------------------------------------------------------------|
|"[..]                                                                         |
|                                                                              |
|I want to invoke this procedure repeatedly on a particular buffer such that   |
|each invocation picks up where the previous invocation left off. For example  |
|                                                                              |
|Ok        : Boolean := True;                                                  |
|Index_Fst : Natural := Buffer'First;                                          |
|Index_Lst : Natural;                                                          |
|...                                                                           |
|                                                                              |
|while Ok and Index_Fst <= Buffer'Last loop                                    |
|  Do_Something(Buffer, Index_Fst, Index_Lst, Ok);                             |
|  Index_Fst := Index_Lst + 1;                                                 |
|end loop;                                                                     |
|                                                                              |
|The problem with this code is that the assignment to Index_Fst inside the loop|
|might raise Constraint_Error if Index_Lst = Buffer'Last after Do_Something    |
|finishes. I can work around this problem but my solutions tend to be rather   |
|ungainly looking. Surely there must be an easy way to handle this.            |
|                                                                              |
|Peter"                                                                        |
|------------------------------------------------------------------------------|

You seemed to dislike the good idea of using different ranges for the
cursors and the array mentioned elsewhere in this thread.

So how about something like
...
Index_Lst : integer := Buffer'First-1; --Hmm, perhaps I have merely
                                       --moved your disliked extra 1.
...

while Ok and Index_Lst + 1 <= Buffer'Last loop
  Index_Fst := Index_Lst + 1;
  Do_Something(Buffer, Index_Fst, Index_Lst, Ok);
end loop;
?

It is a pity that I have introduced code cloning, but looping without
sticking to predominant forms can have this consequence in any
language I can think of (well, just the languages which have already
been defined, that is, excluding languages we can devise).

I really do not approve of the names Index_Fst and Index_Lst. How many
people reading this have still not noticed Index_Fst is not in this
version's condition? Be candid.

I wish Ada success on student satellites!

Regards,
Colin Paul

Re: Processing array subsections, a newbie question.

[Simon Wright]

Colin Paul Gloster <Colin_Paul_Gloster@ACM.org> writes:

> I really do not approve of the names Index_Fst and Index_Lst.

Quite agree. What's wrong with First and Last? (or even if it wasn't
obvious already Index_First, Index_Last).

Re: Processing array subsections, a newbie question.

[Peter C. Chapin]

Simon Wright wrote:

> Colin Paul Gloster <Colin_Paul_Gloster@ACM.org> writes:
> 
>> I really do not approve of the names Index_Fst and Index_Lst.
> 
> Quite agree. What's wrong with First and Last? (or even if it wasn't
> obvious already Index_First, Index_Last).

'First' and 'Last' are reserved by SPARK as FDL identifiers. Similarly 'Start'
and 'Finish' are reserved by SPARK. Obviously 'Begin' and 'End' is not going
to work either since they are reserved by Ada. So while I rather
dislike 'Fst' and 'Lst' I found it awkward finding a suitable matched pair of
names that would otherwise convey my intention.

In my actual program the index variables are named differently than in my
example anyway. However, I admit that I have used 'Fst' and 'Lst' at times in
my code since I couldn't think of anything else that wasn't reserved. I
probably lack imagination.

Peter

Re: Processing array subsections, a newbie question.

[Jeffrey R. Carter]

Peter C. Chapin wrote:
> 
> In my actual program the index variables are named differently than in my
> example anyway. However, I admit that I have used 'Fst' and 'Lst' at times in
> my code since I couldn't think of anything else that wasn't reserved. I
> probably lack imagination.

Initial and Final? Commence and Conclude? Origin and Destination? Alpha and Omega?

-- 
Jeff Carter
"Apart from the sanitation, the medicine, education, wine,
public order, irrigation, roads, the fresh water system,
and public health, what have the Romans ever done for us?"
Monty Python's Life of Brian
80

Re: Processing array subsections, a newbie question.

[Simon Wright]

"Peter C. Chapin" <pcc482719@gmail.com> writes:

> Simon Wright wrote:
>
>> Colin Paul Gloster <Colin_Paul_Gloster@ACM.org> writes:
>> 
>>> I really do not approve of the names Index_Fst and Index_Lst.
>> 
>> Quite agree. What's wrong with First and Last? (or even if it wasn't
>> obvious already Index_First, Index_Last).
>
> 'First' and 'Last' are reserved by SPARK as FDL identifiers. Similarly
> 'Start' and 'Finish' are reserved by SPARK. Obviously 'Begin' and
> 'End' is not going to work either since they are reserved by Ada. So
> while I rather dislike 'Fst' and 'Lst' I found it awkward finding a
> suitable matched pair of names that would otherwise convey my
> intention.
>
> In my actual program the index variables are named differently than in
> my example anyway. However, I admit that I have used 'Fst' and 'Lst'
> at times in my code since I couldn't think of anything else that
> wasn't reserved. I probably lack imagination.

Oops, I didn't know that.

A shame that to make code provable you have to make it unreadable.

Re: Processing array subsections, a newbie question.

[Phil Thornley]

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

Re: Processing array subsections, a newbie question.

[Peter C. Chapin]

Simon Wright wrote:

> Oops, I didn't know that.
> 
> A shame that to make code provable you have to make it unreadable.

The naming issue isn't that big a problem in practice. I've only hit it this
once so far. With a little effort I could probably come up with something
better that doesn't clash.

Peter

Re: Processing array subsections, a newbie question.

[Peter C. Chapin]

Phil Thornley wrote:

> 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).

That's cool. Good to know!

Peter

Re: Processing array subsections, a newbie question.

[Yannick Duchêne (Hibou57)]

Le Tue, 15 Jun 2010 13:27:06 +0200, Peter C. Chapin <pcc482719@gmail.com>  
a écrit:
>> 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).
>
> That's cool. Good to know!
>
> Peter
If you use it, just be careful that names in VC and simplified VC files  
will be changed (just wanted to noticed so you will not feel lost).


-- 
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.

Re: Processing array subsections, a newbie question.

[Niklas Holsti]

Jeffrey R. Carter wrote:
> Niklas Holsti wrote:
>>...
>>       exit when Index_Fst >= Buffer'Last;
> ...
> 
> So it looks to me as if the correct test is
> 
> exit when Index_Lst [>]= Buffer'Last;

I agree. As too often happens, I was reading (and copying) what I 
expected to see, and not what was actually written. Five strokes of the 
lash for me...

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: Processing array subsections, a newbie question.

[Ludovic Brenta]

"Jeffrey R. Carter" <spam.jrcarter.not@spam.acm.org> writes:
> So it looks to me as if the correct test is
>
> exit when Index_Lst [>]= Buffer'Last;
>
> (Maybe Brenta meant this, and mistyped it; the variable names are very
> similar. Using _First and _Last might make such an error more
> obvious.)

Yes, that's what I meant, and I agree with you.  In addition, Stephe's
suggestion to replace Index_Fst and Index_Lst with a single Index,
passed in out to Do_Something, is even better.

-- 
Ludovic Brenta.