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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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!news2.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed00.sul.t-online.de!t-online.de!storethat.news.telefonica.de!telefonica.de!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: Generic Package Newsgroups: comp.lang.ada User-Agent: 40tude_Dialog/2.0.15.1 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH References: <1177539306.952515.222940@s33g2000prh.googlegroups.com> <1177601484.444701.171560@r35g2000prh.googlegroups.com> <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> <1177944533.13970.17.camel@localhost> Date: Mon, 30 Apr 2007 18:29:18 +0200 Message-ID: <2aq08qbvw0ym$.1rquampzo7o53.dlg@40tude.net> NNTP-Posting-Date: 30 Apr 2007 18:28:56 CEST NNTP-Posting-Host: ba3a2914.newsspool1.arcor-online.net X-Trace: DXC=L]7P;R0Fb74Fo<]lROoR1Fl8W>\BH3Y23:H4CfN[Y79DNcfSJ;bb[5IRnRBaCdiS4@F]XGk> 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