Re: Generic Package

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

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