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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.albasani.net!newsfeed.xs3.de!io.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED.rrsoftware.com!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Studying and Maintaining GNAT, Is There Any Interest in a New Group? Date: Tue, 4 Sep 2018 17:18:08 -0500 Organization: JSA Research & Innovation Message-ID: References: <309225242.556906218.575482.laguest-archeia.com@nntp.aioe.org> <2145221813.556924687.162377.laguest-archeia.com@nntp.aioe.org> <3892c779-2924-405c-b88d-19389fc5ba3e@googlegroups.com> <1ceec6d8-c5c4-49b1-9808-a3580bba3f8e@googlegroups.com> Injection-Date: Tue, 4 Sep 2018 22:18:09 -0000 (UTC) Injection-Info: franka.jacob-sparre.dk; posting-host="rrsoftware.com:24.196.82.226"; logging-data="8624"; mail-complaints-to="news@jacob-sparre.dk" X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Response X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.7246 Xref: reader02.eternal-september.org comp.lang.ada:54317 Date: 2018-09-04T17:18:08-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:pmg5ec$rr7$1@gioia.aioe.org... > On 2018-09-01 00:42, Randy Brukardt wrote: ... >>> BTW, I prefer to fold constants before generating the tree. I.e. when >>> Evaluate is called it returns either a value ("constant" node) or a new >>> "dynamic" node. >> >> In Ada, you can't do folding until you know what the operations are, and >> you >> don't know that until after resolution (that is, "*" could be predefined, >> which you can fold, or user-defined, which you probably can't fold, and >> certainly can't treat as static). > > I meant folding universal constants. During/after type resolution one > could generate the next tree and fold resolved constants then. Ystill can't fold those in Ada. Consider: A : constant Saturated := 2 + 2; You can't fold "2 + 2" without doing resolution first, since Ada says that a user-defined "+" operator would be used here (which is probably the case for a Saturated type). It's pretty rare that the universal operations get used in Ada code. To fold this expression (assuming a typical implementation for saturated "+"), you'd have resolve the expression, inline the "+" code, and then fold that. ... >> I have a different vision of static verification than you do; I'm >> primarily >> focused on static verification of Ada's dynamic checks. (Since that >> includes >> pragma Assert and the like, you can verify almost everything this way.) > > It is OK, but low-level. One cannot organize such checks in a way of type > checks, which have inheritance, parameter matching, composition of new > types. You lose a lot. Not everything can be checked by types, of course. Well, actually, class-wide preconditions/postconditions do in fact have those characteristics. Of course, you need an OO design to take advantage of that -- but the point is you don't have to do *everything* with types. Randy.