Re: Generic Package

[Georg Bauhaus <bauhaus@futureapps.de>]

On Mon, 2007-04-30 at 14:16 +0200, Dmitry A. Kazakov wrote:

> > So it is not a question of trusting the iterator but rather
> > a mere consequence of trust in the iterator being defined
> > as required by the specification of iterator.
> 
> But you could not present any formal specification of.
> 
> Consider the program that counts elements of a set:
> 
>    C : Protected_Integer;
>    procedure Count is
>    begin
>       C.Inc;
>    end Count;
> begin
>    C.Set (0);
>    foreach S do Count;


"The following iterator is defined:

    generic
       with procedure P(C: Cursor);
    procedure foreach(S: Set);

"The foreach procedure operates as if the following body
were written

    procedure foreach(S: Set) is
       C: Cursor;
    begin
       C := first(S);
       while has_element(C) loop
          P(C);
          next(C);
       end loop;
    end;

"The set S is locked while foreach is executing."

> How could you prove that C.Get = S'Length?

Given
   Sum: Integer := 0;
   procedure Count(C: Cursor) is
   begin
      Sum := Sum + 1;
   end;
   procedure how_many is new foreach(P => Count);
Still impossible to show the above after the first run?


> >>> Is there iteration in the following SETL expression?
> >>> 
> >>>   Result := { x : x in {1, 3, 24, 17, 11} | P(x) };
> >> 
> >> Iteration in what? In the language construct? In Result? Consider a
> >> possibility that Result were computed at compile time. Would it still be
> >> iteration?
> > 
> > That's the point, there is iteration in this set former, but it
> > happens behind the scene: on an AS-IF basis, it does not even matter
> > when (or even if) iteration is happening;
> 
> Right, that is _the_ point. What is the reason to call this "iteration,"
> rather than an operation constructing a new set?

(It isn't called iteration, actually. The above is a set former.
This was meant to be used for clarification, i.e. to learn what
iteration might mean.)