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,585fd78267abd80c X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news1.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsfeed00.sul.t-online.de!t-online.de!news.karotte.org!news2.arglkargh.de!noris.net!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Wed, 30 Jul 2008 19:45:03 +0200 From: Georg Bauhaus User-Agent: Thunderbird 2.0.0.16 (Macintosh/20080707) MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: On pragma Precondition etc. References: <4889886d$0$18827$9b4e6d93@newsspool2.arcor-online.net> <6etsi6F8mbmbU2@mid.individual.net> <488efc8d$1@news.post.ch> <488f26e8$0$20705$9b4e6d93@newsspool4.arcor-online.net> <1668bcqbkwlun$.mzzrx5m5ug2t$.dlg@40tude.net> <488f3d67$0$20703$9b4e6d93@newsspool4.arcor-online.net> <13nqxvysv2w75.bpxxsup39g9u$.dlg@40tude.net> <48902f08$0$1064$9b4e6d93@newsspool3.arcor-online.net> <1lt840f6z5lva.8rilgn0ds47u$.dlg@40tude.net> In-Reply-To: <1lt840f6z5lva.8rilgn0ds47u$.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: <4890a8a0$0$11740$9b4e6d93@newsspool1.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 30 Jul 2008 19:45:04 CEST NNTP-Posting-Host: 47d3512f.newsspool1.arcor-online.net X-Trace: DXC=agmkblK2fN<^cW`WBF>WQ4Fo<]lROoR14nDHegD_]R5X\LZO6hn:E:;9OJDO8_SK6NSZ1n^B98i:bInH4iVS0c; X-Complaints-To: usenet-abuse@arcor.de Xref: g2news2.google.com comp.lang.ada:7117 Date: 2008-07-30T19:45:04+02:00 List-Id: Dmitry A. Kazakov schrieb: > On Wed, 30 Jul 2008 11:06:16 +0200, Georg Bauhaus wrote: >> (1) the precursor's contract-type (up the derivation hierarchy) >> (2) the profile >> >> So given >> >> function Foo(X, Y: Integer) return Whatever; >> >> denote the precondition of its "contract-type" by something like >> >> Foo'Precondition; > > > In presence of: > > subtype My_Integer is Integer range 1..500; > type My_Whatever is new Whatever with private; > > what are the preconditions of Foo defined on the tuples: > > Integer x My_Integer x Whatever > My_Integer x Integer x Whatever [some more combinations] Any preconditions are those that you specify, of course. They don't magically start to exist[*], and DbC adds no magic for excluding subtle contradictions. Of course, Boolean expressions involving the subprogram parameters will be checked by the compiler. Just like with Ada; they are checked now, pragma Precondition(); with some rules for what can be part of . No more, no less. Now the rules that say how preconditions are to be logically connected when overriding. Go ahead! First, do you want a derived object to be a suitable argument for a parent's procedure? With or without preconditions, arguments may meet both: the type constraints that Ada has to offer, and the DbC constraints. Let's see, type Whatever is tagged private; procedure Foo(Item: Whatever); -- pre: permissible values of Item type My_Whatever is new Whatever with private; overriding procedure Foo(Item: My_Whatever); -- pre: permissible values at least as above X: Whatever'Class := ...; begin Foo(X); end; In this case object X must satisfy the parent's preconditions for calling Foo and the child's preconditions for calling its Foo. So the rule would be to "weaken" the precondition in child overridings. The phrase "at least" from the comment on the overridden Foo translates into "or else". Theory then says, "When overriding, only add permissible values, do not remove any." For extended records I find this rule strikingly obvious, because every component added to the parent type will enlarge the set of values available in the child type. Seen in this light, range 1 ... 500 takes away values from Integer'range. (Not surprisingly, since it is a constraint.) subtype My_Integer is Integer range 1 .. 500; overriding procedure Bar(Item: My_Whatever; Num: My_Integer); With or without DbC, it seems reasonable to me to expect that Bar fails when it gets an argument for Num outside range 1 .. 500. Say it fails with a Constraint_Error. This exceptional behavior is already illustrating why the DbC idea of having a 'Constraint on a type makes sense. It is already working for subtypes now. With or without DbC, you can always be troubled by the typical variance problems, for which, as you have said before, there is no universally good solution. Many shrug when they are more busy with the practical benefits of DbC. ___ [*] Sofcheck's tools can extract a number of assertions. There is also an Eiffel(?) tool doing similar things. But this is beside the point when you want to design a provable DbC component (typically, a tagged type). It adds nothing in the sense of DbC, just more assertions for us that help with analyzing our programs which would typically lack assertions.