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,585fd78267abd80c X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!newsfeed.straub-nv.de!uucp.gnuu.de!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail From: "Dmitry A. Kazakov" Subject: Re: On pragma Precondition etc. 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: <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> <4890a8a0$0$11740$9b4e6d93@newsspool1.arcor-online.net> Date: Thu, 31 Jul 2008 10:12:40 +0200 Message-ID: <13z82kclqrff3$.6ih7736s42ql$.dlg@40tude.net> NNTP-Posting-Date: 31 Jul 2008 10:12:40 CEST NNTP-Posting-Host: 34f5f855.newsspool4.arcor-online.net X-Trace: DXC=3VQ?KdD7S]:lIh70@\BH3Y2V489E=X\SV0DNcfSJ;bb[5FCTGGVUmh?4LK[5LiR>kg2WWF0cmhoRD= X-Complaints-To: usenet-abuse@arcor.de Xref: g2news1.google.com comp.lang.ada:1392 Date: 2008-07-31T10:12:40+02:00 List-Id: On Wed, 30 Jul 2008 19:45:03 +0200, Georg Bauhaus wrote: > 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[*], Of course they do. If there is no explicit precondition specified for an argument X of the type T, it still exists, and is: X in T [and true] > 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? Yep, substitutability is it all about. > With or without preconditions, arguments > may meet both: the type constraints that Ada has to offer, > and the DbC constraints. The point is that when you hang some contracted constraints on the parameters of a subprogram, you implicitly define a set of derived types constrained to that. The subprogram become a primitive operation of these derived types. [a liberal explanation of LSP skipped] > 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. No, it fails at compile time, provided, 1 .. 500 goes into the contract, because the result is not LSP-conform. But the question was different. It was about composition of conditions in presence of tuples of parameters. You consider each parameter and its contracted constraints independently, this is wrong. > 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. Wrong. Ada constraints are not contracts. A constrained subtype when it inherits primitive operations of the unconstrained base type, also does the contracts of these operations in full. To be LSP-conform these contracts shall include Constraint_Error. Otherwise, that would violate substitutability. Ada assumes Constraint_Error in all contracts, which is quite unfortunate for static analysis. But it was necessary to do because its exceptions are not contracted. > Many shrug when they > are more busy with the practical benefits of DbC. I don't buy it. Practice unsupported by a sound theory is shamanism. ------ BTW, we could drop the idea of making conditions contracted. Instead of that, we would consider constraints in the sense of Ada subtypes. Which is the model used in Eiffel. In that case it would be all dynamic, run-time. [Contracted constraints are more like SPARK model] But in any case the problem would remain. We would have to introduce anonymous subtypes of tuples of [sub]types. In both cases we need a [sub]type to associate the constraint with. We cannot do it for a subprogram, except the case when it has only one parameter. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de