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,29d8139471e3f53e X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,UTF8 Path: g2news1.google.com!news3.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!193.201.147.81.MISMATCH!feed.xsnews.nl!border-1.ams.xsnews.nl!feeder.news-service.com!newsfeed.straub-nv.de!uucp.gnuu.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Fri, 24 Sep 2010 11:10:57 +0200 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.6; en-US; rv:1.9.2.9) Gecko/20100915 Thunderbird/3.1.4 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Preventing type extensions 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> <8f6cceFrv2U1@mid.individual.net> <135a7dc9-3943-45e4-884b-3cc6bce3db0a@q18g2000vbm.googlegroups.com> <10rutrnp4yp1b$.vxcbtginicg9.dlg@40tude.net> <1rwwxbzfj78eh.6l7isp9fciba$.dlg@40tude.net> <4c98e745$0$7667$9b4e6d93@newsspool1.arcor-online.net> <1qwl6jiun2mik$.s1k2xnzg8dv6$.dlg@40tude.net> <118qmxho82l2o$.2hnfi4z6468h$.dlg@40tude.net> In-Reply-To: <118qmxho82l2o$.2hnfi4z6468h$.dlg@40tude.net> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Message-ID: <4c9c6b21$0$7660$9b4e6d93@newsspool1.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 24 Sep 2010 11:10:57 CEST NNTP-Posting-Host: 4e1bcb69.newsspool1.arcor-online.net X-Trace: DXC=YV_m>7McglHgj[ZPFj7ehOic==]BZ:afN4Fo<]lROoRA<`=YMgDjhgBgaiRg1na0bBPCY\c7>ejVH0@n5M=BFK>E8CA_Rgg[]^F X-Complaints-To: usenet-abuse@arcor.de Xref: g2news1.google.com comp.lang.ada:14227 Date: 2010-09-24T11:10:57+02:00 List-Id: On 9/23/10 10:49 PM, Dmitry A. Kazakov wrote: > On Thu, 23 Sep 2010 21:00:01 +0100, Simon Wright wrote: > >> "Dmitry A. Kazakov" writes: >> >>> Gosh, it was no more than just this: if horse is an animal that does >>> not imply they are interchangeable. Compare: "all horses have hoofs" >>> and "all animals have hoofs." >> >> I don't see your point. > > It was: the type /horse/ is not the type /animal/. That is not because of > Ada's choice to keep them apart, it is because they are behaviorally > (semantically) different. > >> You could make a near-infinity of operations on Animal like has-hooves, >> has-tentacles etc but that would be silly. The only ops that make sense >> at the Animal level are ones shared by all animals. > > All primitive operations are already shared, if it were only about type > checks there would be nothing to discuss. Ada checks types. > > Beyond nominal checks, comparing two related types like horse and animal > one considers substitutability. S is substitutable for T when any predicate > P(T) remains true after substitution S for T. LSP subtype as defined by > Liskov& Wang Wing, Jeanette M. > are those maintaining substitutability. (All possible > predicates exhaustively determine what in OO is called behavior. This is > why Liskov& Wang named it "behavioral notion of subtype.") My example > illustrated existence of predicates turning false. Thus horse is not animal > and animal is not horse (yet *a* horse is *an* animal). It is a tautology: > a subset which is the whole set is not the whole set. [Just trying to follow.] "Subtype Requirement: Let Φ(x) be a property provable about objects x of type T. Then Φ(y) should be true for objects y of type S where S is a subtype of T." (Where "property" is defined a little later.) The authors emphasize that while Stack and Queue may share operations, this type checked sharing of operations is not enough. It does not guarantee that the programs will work the same way if either is used, and likely not as expected. Not working correctly. "Properties of an object's behavior" refers to states and to sequences of states, as effected by prim ops: Invariants: P(state) = True for all states. History properties: P(state_1, state_2) = True for pairs of states. I think that in your example, Horse (S) is not a subtype of Animal (T), since Has-Hooves(x) cannot be proved for any x of type Animal. A Horse object can substitute an Animal object IFF all prim ops of Horse, including "extra methods", can all be expressed in terms of Animal's prim ops *and* respecting the conditions placed on the objects states and state sequences. The programs must behave the same, for Animals and Horses. (That's how I have understood the model so far.) Correct? That is, when I assign an object of type Horse to a variable of type Animal, then what matters is that the Animal program still behaves as would be correct for an Animal program. But not necessarily for a Horse program: The "apparent" type (L&W) of objects will be Animal, a specific type in Ada, and neither aliasing nor objects being used in a different context (view conversions in another partition, for example) will produce a state not correct for Animals. If the program behaves differently when I use a Horse object where an Animalis expected, then Horse is not a behavioral subtype of Animal. Correct? So, up to here, nothing in Liskov & Wing's Subtype Requirement (as quoted above) corresponds to Ada's Animal'Class. [Just to make sure I get the words right.] Correct?