Re: Studying and Maintaining GNAT, Is There Any Interest in a New Group?

["Randy Brukardt" <randy@rrsoftware.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> 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.