From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,229ea0001655d6a2
X-Google-Attributes: gid103376,public
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news1.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed00.sul.t-online.de!t-online.de!newsfeed.freenet.de!news.n-ix.net!news2.arglkargh.de!news.visyn.net!uucp.gnuu.de!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Newsgroups: comp.lang.ada
Subject: Re: Generic Package
From: Georg Bauhaus <bauhaus@futureapps.de>
In-Reply-To: <2aq08qbvw0ym$.1rquampzo7o53.dlg@40tude.net>
References: <1177539306.952515.222940@s33g2000prh.googlegroups.com>
	 <1177601484.444701.171560@r35g2000prh.googlegroups.com>
	 <pcp92sp50q98$.lad523qlftgm.dlg@40tude.net> <m2zm4udcqt.fsf@mac.com>
	 <degsdvcu9wwi$.1j7dffe23bgq5$.dlg@40tude.net>
	 <9eejm6rqip.fsf@hod.lan.m-e-leypold.de>
	 <19qllkvm6ut42$.1iqo74vjgmsrv$.dlg@40tude.net>
	 <1177801611.10171.32.camel@localhost.localdomain>
	 <1woad6hn9idy2$.6otnwphc1o0h$.dlg@40tude.net>
	 <1177929029.6111.34.camel@localhost>
	 <maztz79bn7ey.1bxuei6uqjiwu.dlg@40tude.net>
	 <1177944533.13970.17.camel@localhost>
	 <2aq08qbvw0ym$.1rquampzo7o53.dlg@40tude.net>
Content-Type: text/plain
Content-Transfer-Encoding: 7bit
Message-ID: <1177953892.13970.23.camel@localhost>
Mime-Version: 1.0
X-Mailer: Evolution 2.10.1 
Date: Mon, 30 Apr 2007 19:24:52 +0200
Organization: Arcor
NNTP-Posting-Date: 30 Apr 2007 19:19:10 CEST
NNTP-Posting-Host: fb133339.newsspool2.arcor-online.net
X-Trace: 
 DXC=mY0lQVKAD?QU6b:FjPaGjQA9EHlD;3YcR4Fo<]lROoRQ8kF<OcfhCO[Yl;ZbJ?bd7Q=kbmW`a1fGWC`2T@AUZfC[11di?5oYkCY
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news1.google.com comp.lang.ada:15426
Date: 2007-04-30T19:19:10+02:00
List-Id: <comp.lang.ada>

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

> > "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,

I was tempted to add

         C := first(S); -- where first picks any as defined for the
                        -- `first`  operation on sets; gimmeacursor(S);

>  which is not well-ordered and 
> thus does not have visible implementations of

As I said, Iterate operates as if it were implemented the way shown.
I had intended to base the argument on your prior remark that we
can specify the preconditions on next etc. I claim that we can
give a meaningful definition of First, too, which is not given by
the usual meaning of First; we could call it Frumble if you like.



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

> The set 
> is declared unordered.

Yes. An iterator will work without an externally visible order.


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

No, I only have to combine the semantics of foreach as specified
previously, ":=", "+", etc. Then I can show that I get what I
asked for.