Re: How to get nice with GNAT?

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

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:hz0z7hi7czmw$.1qfhyt5f4awot.dlg@40tude.net...
> On Mon, 1 Dec 2014 16:25:28 -0600, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:1g5ttpzi8eywc$.1gluj9evlmeus.dlg@40tude.net...
>> ...
>>> The idea that all/most/some bugs should somehow manifest their wrong
>>> behavior in exceptions is dubious.
>>
>> Fascinating. I'd say the reverse: that almost all bugs quickly manifest
>> themselves in an exception (at least in well-designed Ada code). For
>> instance, I tend to make off-by-one errors in index calculations. Such
>> errors almost always result in a Constraint_Error when the index is used.
>
> The index may slip toward another side. Why do you expect that any wrong
> index would always be out of the range?

"Any wrong index"? I never said that. At some point, the off-by-one error 
will be out of the expected range and a Constraint_Error will result. And 
that will directly show the problem.

>> Similarly, in Janus/Ada, we've sometimes passed the wrong entity to a
>> subprogram; that almost always shows up as a Constraint_Error detecting 
>> the
>> use of a non-existent variant. (If a routine expects a symboltable 
>> pointer
>> to an object, and gets a package, the components it needs aren't going to 
>> be
>> there.)
>
> In such cases I just use tagged types. The problem here is in weakly-typed
> design, which makes run-time type errors possible.

Huh? The thing passed is an access-to-a-symbol, which is an 
access-to-variant-record in an untagged design, or an 
access-to-class-wide-symbol in a tagged design. Either way, you'll get a 
run-time error. In Ada 2012, you could use a predicate on the parameter in 
order to make the check sooner, but it still will be a runtime check.

I should note that most of my compiler work was with the code that converts 
semantic information into intermediate code. That means I'm taking an 
expression tree (with "Name" nodes decorated with symbol pointers) and 
converting it to a form closer to machine code. These can't be primitive 
operations of the symbol type (it might have been possible to make them 
primitive operations of the expression tree nodes, but that's irrelevant to 
this point), so the only realistic possibility is going to be 
access-to-something with associated runtime checks.

In may experience, most problems come down to managing combinations of 
several kinds of objects (in the abstract sense, not the Ada sense), and 
it's not sensible to try to do that in any sort of statically typed manner. 
(Especially in Ada, where only one inheritance tree can be primitive, but 
it's also true in general, because there are too many combinations to deal 
with.) Strong typing is great to eliminate gross errors (like passing an 
expression node when a symbol entry was meant -- as both are represented as 
access types, they can easily be confused), but it's not going to catch the 
lower-level mistakes.

>> Indeed, the recent history of Ada includes more and more ways to specify
>> what is expected/needed for a parameter/object/component. Null exclusions
>> (Ada 2005), preconditions, and predicates (Ada 2012) are all ways to more
>> closely tell the compiler what is intended.
>>
>> The next step, IMHO, is to include exception contracts that effectively
>> require exceptions not to occur. If they in fact do occur, then the 
>> program
>> is wrong and will be rejected by the compiler. That means that 
>> "unexpected"
>> Constraint_Errors will be detected statically and thus the manifestation 
>> of
>> many bugs can be detected -- thus eliminating the bugs at the source.
>>
>> Of course, once that next step is taken (and I mean in the context of the
>> full Ada language, not just some simple subset like SPARK), then you'll
>> probably be right. But that's still some distance in the future.
>
> No. Statically eliminated bugs don't manifest themselves at all. They make
> the program illegal.

Exactly. Which means that they never get to runtime at all -- which is the 
ultimate goal for making programs more correct.

> The point is that bugs in a legal program may expose any behavior [within
> of possible]. There is no way to predict this behavior and thus hoping 
> that
> it would become an exception or setting some variable in some way is
> dubious.
>
> SPARK or any language design would not change this, the bugs they catch 
> are
> caught, which is good, but the rest will act as it always does.

Of course, no technology could ever catch every bug. But the point here is 
to reduce the universe of legal possibilities, hopefully to the limit so 
that either an exception is raised or the program works as designed. Note 
that the latter still could in fact be buggy, because a lot of programs work 
as designed but still don't do what they are supposed to do (at the human 
level). No technology could ever eliminate that case, as such it's not worth 
even talking about other than to acknowledge its existence.

                                                             Randy.