Re: Generic Package

On Mon, 30 Apr 2007 16:48:53 +0200, Georg Bauhaus wrote:

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

You forgot that first is not defined on Set, which is not well-ordered and
thus does not have visible implementations of first, last, next, prev etc
in its interface. It has Length, =, /=, :=, and, or, xor, /, Empty, in, not
in. [*]

while has_element(C) loop
P(C);
next(C);
end loop;
end;

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

Concurrency is not the issue. Some ordered sets might become unordered in
presence of concurrent access. But the reason is irrelevant here. The set
is declared unordered. Locking it cannot not change that, unless you looked
in the implementation.

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?

No, that would not be a proof, only a test. To make a proof out of it, you
have to run this test on all possible programs with all possible sets.

---------
* If Element of unordered Set is itself ordered and countable, then you
could solve the problem by combining Element'Succ with "in" membership
test. I.e. Element would give you an order. But in general case there could
be no Element'Succ.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
.

Relevant Pages

  • Re: IEnumerable is strange
    ... That's exactly what 'yield return' is: ... int foo() ... and similarly investigate how foreach is ... The function implementing the iterator is technically never entered. ...
    (microsoft.public.dotnet.languages.csharp)
  • Re: recursive GetEnumerator()
    ... it couldn't do that - don't forget that foreach could be in one ... The way I implemented it before in c was to pass a function to the iterator, ... I gues if the type isnt completly fixed at compile time this isnt possible ... There's a big difference between Reflector and reflection... ...
    (microsoft.public.dotnet.languages.csharp)
  • Re: Features new to Java 5.0 rated today
    ... But would it not be useful if the foreach statement could go over an ... But what if the Iterator had been used previous to being passed to the ... If you're not thinking about the entering state of a Collection before ... puting it into a foreach statement you're.... ...
    (comp.lang.java.advocacy)
  • Re: Question about Iteration and forEach
    ... Not want to get in a coding contest but you can also encapsulate this in an iterator. ... // any IEnumerable collection in a foreach statement. ... foreach (Item itemCur in MyCollection) ... // Do some stuff with itemPrev. ...
    (microsoft.public.dotnet.languages.csharp)