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,29d8139471e3f53e X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news3.google.com!feeder.news-service.com!newsfeed.kamp.net!newsfeed.kamp.net!news.qsc.de!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: Securing type extensions 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: <87iq2bfenl.fsf@mid.deneb.enyo.de> <874odv9npv.fsf@ludovic-brenta.org> <87y6b7cedd.fsf@mid.deneb.enyo.de> <66a3704c-54f9-4f04-8860-aa12f516134b@t3g2000vbb.googlegroups.com> <87d3sib44t.fsf@mid.deneb.enyo.de> <134q4k2ly2pf4$.17nlv1q6q5ivo.dlg@40tude.net> <4c8dec8e$0$6990$9b4e6d93@newsspool4.arcor-online.net> <4c8e3f44$0$6769$9b4e6d93@newsspool3.arcor-online.net> <4c8e87f8$0$6877$9b4e6d93@newsspool2.arcor-online.net> <4c8f4833$0$6763$9b4e6d93@newsspool3.arcor-online.net> Date: Tue, 14 Sep 2010 14:22:14 +0200 Message-ID: <2ka8sfdvyvil.1k714obgzgj3a.dlg@40tude.net> NNTP-Posting-Date: 14 Sep 2010 14:22:14 CEST NNTP-Posting-Host: 84d7646e.newsspool2.arcor-online.net X-Trace: DXC=OlFEZK0;79_AX0F2i> On Tue, 14 Sep 2010 12:02:28 +0200, Georg Bauhaus wrote: > I'm asking about visibility and how it can possibly help ascertaining > that user supplied subprograms are trustworthy---which is, by > definition, not the same thing as "safe". Hmm, how "trustworthiness" corresponds to correctness and type safety? > So I'm speaking about trust and operations not known yet, in the > presence of user extensible types. All operations are known. Dispatching call always call a *known* operation, because a primitive operation is defined on the whole class. What you call unknown is late binding to a *part* of the body of the operation. It is no less known as sqrt taken from the standard library and resolved by the linker. It is separation of implementation and interface, after all. > Your_Overriding (My_T'Class (Some_Object)); > > Some_Object is of a type that may not exist yet when I write > the body surrounding the above. So can the computer, where the program is supposed to run. The category of developing time is meaningless to the program semantics. > If so, what is the foundation of trust in this O-O style callback scenario? See above. It is type safe. It is possibly incorrect. More elaborated contracts are applied to the *visible* specification, more can be said about correctness. No difference to sqrt, BTW. > I'm asking for the degree to which Ada's ___, ___, ... can establish > trust. That's not the same thing as those purely mechanical static > safety properties of programs. It is what human parties rely on when > calling user supplied prim ops with LSP enacted in some event > driven parser, for example. Let us not go into a discussion why LSP does not work. If you want to be sure about substitutability it is better to call it so, because LSP is misleading, inconsistent and wrong. So, a member of a class is *always* substitutable for an operation defined on the class. You cannot find anything more here without going into contracts beyond mere types. Ada stops here and this is unspecific to dispatch. So see above. SPARK has to tell more. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de