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,UTF8 Path: g2news1.google.com!news4.google.com!proxad.net!proxad.net!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail Newsgroups: comp.lang.ada Subject: Re: Generic Package From: Georg Bauhaus In-Reply-To: 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> <2aq08qbvw0ym$.1rquampzo7o53.dlg@40tude.net> <1ieq3io2d6nnq$.13818v3y35gnr.dlg@40tude.net> <1178010142.6695.29.camel@localhost.localdomain> Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Organization: # Message-Id: <1178026941.16837.88.camel@localhost.localdomain> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Date: Tue, 01 May 2007 15:42:21 +0200 NNTP-Posting-Date: 01 May 2007 15:42:22 CEST NNTP-Posting-Host: 94ffca44.newsspool4.arcor-online.net X-Trace: DXC=M5N_DL?^k=WaAeROF2PWMQ4IUK On Tue, 2007-05-01 at 12:19 +0200, Dmitry A. Kazakov wrote: > On Tue, 01 May 2007 11:02:22 +0200, Georg Bauhaus wrote: >=20 > > On Mon, 2007-04-30 at 22:04 +0200, Dmitry A. Kazakov wrote: > >> It was that if foreach were a primitive operation > >> defined on an unordered set, then its contract could not be stated. > >=20 > > Every specific Set object (collection of elements) inside a computer ha= s > > a memory layout. >=20 > So the memory layout is a part of the contract? Yes, in the sense that the specifics of memory layout and such are unknown and irrelevant to the client; in particular, no order needs to be specified. However, it is then known that the elements of sets in a computer have said properties. These properties will assign meaning to the phrase "Procedure Foreach calls procedure P once for each element of S" or, put differently but still with just logical references to implementation details, "For each node of the set S, the node will be used as the actual argument of P when P is invoked; this is done once for each node of S in an unspecified order." There isn't much a client (programmer) needs to know about nodes. He or she isn't concerned with implementation details. But the abstract notions of what is implemented provide enough formal information so that the operation of Foreach can be described formally. (Just not in terms of its own inner workings as a postcondition stating foreach in terms of foreach. So what?) As a consequence of this formal description, ("nodes", "called once", "each") I can call Foreach passing a procedure Add_One that increments a count variable when called. Provided there is a query function Length of Set (as is typically the case), then (remove quantifiers if more apt) function Unnamed(S: Set) return Count_Type; -- post: (=E2=88=80s) s in Set [ s.Length =3D Result ] function Unnamed(S: Set) return Count_Type is count_var: Count_Type; procedure Add_One(C: Cursor) is begin count_var :=3D count_var + 1; end; begin count_var :=3D 0; Foreach(S, Add_One'access); -- Claim (=E2=88=80s) s in Set [ s.Length =3D count_var ] -- Proof. Foreach calls Add_One exactly once for each node -- in s. Add_One unconditionally increments Count_Var by 1. -- No other operation changes the value of Count_Var. -- Hence, Count_Var (initially zero) is incremented by 1 for -- each node in s, so Foreach counts the elements of s. =E2=88=8E pragma assert(Length(S) =3D count_var); return count_var; end; If there is no Length defined for Set, the above is still enough, to me at least, to show that this computes the number of elements in a Set using a computer representation even when there is no known order of elements and without knowledge of the actual implementation. I think it is possible to add even more contract clauses almost like the ones you have mentioned: function First(S: Set) return Cursor; -- post: let (Result then t0) =3D (First(S) then Clock), -- (Result' then t) =3D (First(S) then Clock) in -- (=E2=88=80t) t > t0 [ Result /=3D Result' ] As you can see, there is some order again but I don't have to know the order. (Finding a first book (and then the next book) is the job of the librarian, not mine.) > >> To be able to pick a random member <=3D> > >> to have an order. > >=20 > > Can you determine whether one of your sets is empty? >=20 > Sure. I can compare an empty set with the given set. This does not requir= e > picking elements. Uhm, not require the client to pick or the implementation to pick? When two sets A and B are equal iff the same elements belong to both A and B, won't you need at least references to the elements for "=3D" to be called for the elements?