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,UTF8 Path: g2news1.google.com!news3.google.com!proxad.net!news.tele.dk!news.tele.dk!small.news.tele.dk!lnewsinpeer00.lnd.ops.eu.uu.net!bnewsinpeer00.bru.ops.eu.uu.net!emea.uu.net!newsfeed.arcor.de!newsspool4.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="utf-8" Content-Transfer-Encoding: 8bit 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> <2aq08qbvw0ym$.1rquampzo7o53.dlg@40tude.net> <1ieq3io2d6nnq$.13818v3y35gnr.dlg@40tude.net> <1178010142.6695.29.camel@localhost.localdomain> <1178026941.16837.88.camel@localhost.localdomain> <1ozvzzh59ebq8$.yeh9do8s3hig$.dlg@40tude.net> <1178055690.27673.39.camel@localhost.localdomain> Date: Wed, 2 May 2007 12:29:58 +0200 Message-ID: <1gptkhkkk93hj.1n23zmm3go7tc$.dlg@40tude.net> NNTP-Posting-Date: 02 May 2007 12:29:58 CEST NNTP-Posting-Host: aeeadfb2.newsspool3.arcor-online.net X-Trace: DXC=G`_Km6ZgM6[V0Pe9PRnbJ\McF=Q^Z^V3X4Fo<]lROoRQFl8W>\BH3YR985:hD1\EWXDNcfSJ;bb[UFCTGGVUmh?TLK[5LiR>kgR^?UO;M<=4HZ X-Complaints-To: usenet-abuse@arcor.de Xref: g2news1.google.com comp.lang.ada:15461 Date: 2007-05-02T12:29:58+02:00 List-Id: On Tue, 01 May 2007 23:41:31 +0200, Georg Bauhaus wrote: > On Tue, 2007-05-01 at 19:16 +0200, Dmitry A. Kazakov wrote: > >> Apart from obvious uselessness of contracts referencing to the memory >> layout, > > I didn't say that. But I did! (:-)) >> the above is self-contradictory. Memory layout defines an order. It >> also is a part of the contract. > > Memory is not abstract, addresses aren't abstract, In what sense? [ I doubt that you were able to bind objects of a higher level language to "non-abstract memory" in a more or less formal way. It is yet another discussion, we probably should not go into. The states of the memory are associated with some computational states and those with some objects "having" some values. It is a tick Napoleon pastry of abstractions layered over abstractions which you would not be able to flatten. As a practical example consider for I in ... loop -- what is I'Address here? can you specify the transistors I has? ] > The abstraction of the implementation implies the existence > of a possible internal private ordering. No, that is of course wrong. An abstraction of unordered set does not imply anything beyond itself. >>> -- 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. ∎ >> >> So the precondition of Add_One is true? > > The proof mentions that Count_Var is initially zero and that > it is only changed by Add_One. Together with the fact that these > are (1) a local variable and (2) a local procedure > closely tied this should imply that pre: Count_Var = 0. So, the precondition is not constant true, it is Count_Var = 0? Then either 1. N = 1 or 2. The program is incorrect, because for any N > 1 your precondition gets violated on the second call to Add_One. Here you are. You cannot specify the precondition of Add_One without referring to the iteration state. You are caught in a circle of tautologies. >>> 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.) >> >> Librarian is the interface. If it finds first book then that is a publicly >> ordered set = you _can_ know the order without breaking the abstraction. > > ? > The first book might be determined by whatever order the librarian > thinks he should choose this time. No, first = [whatever] order. It is same. > Nothing I could determine beforehand. "Beforehand" means what? I hope it does not that you present one set while dealing with another. Ordering is determined by sole existence of the librarian who can give you a [first] book and continue to do so. > The order(s), if any, isn't/aren't publicly known. It is, if you don't cheat. The procedure was described by me in other post. >>>>>> To be able to pick a random member <=> >>>>>> to have an order. >>>>> >>>>> Can you determine whether one of your sets is empty? >>>> >>>> Sure. I can compare an empty set with the given set. This does not require >>>> 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 "=" to be called for the elements? >> >> No. You have to show that whatever element you took (no matter how) it is >> either in both sets or else in neither: >> >> forall x in S, x in Q >> >> This does not force you to present any method of getting elements from any >> of the sets. > > What's the contract of "in"? One of the set theory. You choose the language and a set of axioms, and likely "in" will be somewhere there. So "in" is in a different position than ordering. In ZF ordered pairs are not fundamental, they are constructed. So we could talk about the contracts of on "ZF hardware." Of course it depends on the hardware. Nobody would construct, say, integers as they are constructed in ZF, because there is the ALU, which we could use instead. So "+" becomes per magic. Same is with foreach, you could have a hardware (axioms) for it. In that case it would have no contract. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de