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!news3.google.com!out01a.usenetserver.com!news.usenetserver.com!in01.usenetserver.com!news.usenetserver.com!news.tele.dk!news.tele.dk!small.news.tele.dk!news-fra1.dfn.de!storethat.news.telefonica.de!telefonica.de!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="us-ascii" Content-Transfer-Encoding: 7bit Reply-To: mailbox@dmitry-kazakov.de Organization: cbb software GmbH References: <1177539306.952515.222940@s33g2000prh.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> <1gptkhkkk93hj.1n23zmm3go7tc$.dlg@40tude.net> <1178106506.17912.33.camel@localhost> Date: Wed, 2 May 2007 15:12:55 +0200 Message-ID: <1d7fjjn90n15q.tz3xkhxpuz5x.dlg@40tude.net> NNTP-Posting-Date: 02 May 2007 15:12:55 CEST NNTP-Posting-Host: 2bc7fe57.newsspool4.arcor-online.net X-Trace: DXC=Ug5=IRF=9QnJ00P1S40fZg4IUKkgb\<0i7JXR On Wed, 02 May 2007 13:48:26 +0200, Georg Bauhaus wrote: > On Wed, 2007-05-02 at 12:29 +0200, Dmitry A. Kazakov wrote: > >>> Memory is not abstract, addresses aren't abstract, >> >> In what sense? > > When you write a Set implementation for a PC, you can specifying > addresses and refer to addresses in a consistent way. But I am not required to do so. BTW 1, it is a quite common programming pattern to share some predefined states of the container, usually empty ones, but not only. An implementation of a container of integers could have a reserved representation for contiguous ranges of integers. For these it would keep only From and To. Now, let you have a container holding 1, 2, 3, can you point me the address of 2 there? Another typical pattern is some f applied to the actually kept values, so "()" actually is a composition f o "()". So what is in the container? BTW 2, it is sort of surprising to have such a discussion in c.l.a., for Ada was one of the first languages introducing a clear distinction between interface and implementation. >> for I in ... loop >> -- what is I'Address here? > > irrelevant without computational model. (I didn't say that the > mentioned abstract addressable node is good for everything. > But even so, it should not be too difficult to come up with an > AS-IF model of how I "work"; otherwise, Ada would have an > insurmountable teaching problem, besides other exegetic trouble.) Huh, argumentation to Turing-completeness is a subject of Godwin's Law... >>> 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, > > The program is correct; the assumption that Count_Var = 0 is > false and not the precondition of Add_One at each time. My fault > being sloppy. > ("Count_Var is initially zero and ... is only changed > by Add_One".) That still does not describe the precondition of. In particular, where it follows that counts S and not something else? S have to appear there. > So there is a well defined > operation going on It might be a well-defined operation, but its outcome is not. >> No, first = [whatever] order. It is same. > > How is "whatever order" defined, exactly, and how can I say whatever > first book will come given a library? Merely by saying/writing "first." That defines a book. >> Ordering is determined by sole existence of the >> librarian who can give you a [first] book and continue to do so. > > That is, ordering is an outcome of the librarians operation, > not of the books. Come on, all orderings are ordered but some orderings are more ordered than others? (:-)) _WHAT_ is the difference? Let you asked somebody to bring you books in their "proper" order. How can you determine if he does not cheat, or just mistakenly used the issue date rather than the birth day of the author written in Roman numerals and ordered according to Unicode positions? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de