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!news4.google.com!proxad.net!proxad.net!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail Newsgroups: comp.lang.ada Subject: Re: Generic Package From: Georg Bauhaus In-Reply-To: <1gptkhkkk93hj.1n23zmm3go7tc$.dlg@40tude.net> 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> <1gptkhkkk93hj.1n23zmm3go7tc$.dlg@40tude.net> Content-Type: text/plain Content-Transfer-Encoding: 7bit Message-Id: <1178106506.17912.33.camel@localhost> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Date: Wed, 02 May 2007 13:48:26 +0200 Organization: Arcor NNTP-Posting-Date: 02 May 2007 13:42:39 CEST NNTP-Posting-Host: 6a9836bf.newsspool4.arcor-online.net X-Trace: DXC=oCiW:^WeGkcIkjb;<8iR=a4IUK 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. > 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.) > can you specify the transistors I has? ] no need. > > 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. I didn't say anything about unordered sets here. I have given a description of an implementation model. > > 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".) > 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. Ok, Ok. There is a reason I didn't specify that as a precondition for Add_One. Add_One adds 1 to whatever initial value Count_Var has. It has the value 0 before the defined procedure Foreach starts operating using Add_One, as described. So there is a well defined operation going on and I can argue about this operation using the formally defined abstraction "Iterator". > 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? > > Nothing I could determine beforehand. > > "Beforehand" means what? It means that it is impossible to predict an order because nothing is known about any order by any client. > 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. > >> 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. OK > Of course it depends on the hardware. OK. Glad to hear someone recognizes the inversion that mathematics brings in. Normative ontology at its best, though :-)