Prev: What is SPARK about?
Next: Improving the first contact with Ada
From: Peter C. Chapin on 12 Jun 2010 15:11
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

From: Yannick Duchêne (Hibou57) on 12 Jun 2010 15:38
Le Sat, 12 Jun 2010 21:11:33 +0200, Peter C. Chapin <pcc482719(a)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.
From: Yannick Duchêne (Hibou57) on 12 Jun 2010 15:41
Le Sat, 12 Jun 2010 21:11:33 +0200, Peter C. Chapin <pcc482719(a)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.
From: Ludovic Brenta on 12 Jun 2010 16:54
"Peter C. Chapin" <pcc482719(a)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;
From: Gene on 12 Jun 2010 21:20
On Jun 12, 4:54 pm, Ludovic Brenta <ludo...(a)ludovic-brenta.org> wrote:
> "Peter C. Chapin" <pcc482...(a)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.
 |  Next  |  Last
Pages: 1 2 3 4 5 6
Prev: What is SPARK about?
Next: Improving the first contact with Ada