Re: Generic-Package Elaboration Question / Possible GNAT Bug.

[Robert A Duff <bobduff@shell01.TheWorld.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On Mon, 21 Nov 2011 08:08:04 -0500, Robert A Duff wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>> 
>>>>> I don't know if Ada keeps that promise for generic bodies, ...
>> 
>> I think it does.  I'd be interested in any counterexamples.
>
> GNAT sometimes reports errors in generic bodies upon instantiation, but I
> am not sure if these are not compiler bugs.

I have seen such compiler bugs in the past.

There are also some cases where GNAT allows representation clauses
in a generic body that might turn out to be illegal in some instances.
But as far as I know, these are optional -- GNAT didn't HAVE to support
them in generic bodies, so this violation of the contract model is
GNAT's, not Ada's.  And it's useful, although nonportable.

>>>...Generic contracts are too weak for that.
>> 
>> Well, it's not that the contracts are too weak.  You just have to
>> consider the entire generic spec (including the private part,
>> unfortunately), as part of the "contract".
>
> That is C++'s approach.  If matching formal parameters does not imply
> legality, that does not look very contracted.

The C++ approach is that the entire template is the "contract"
(which means there really is no contract).
In Ada, at least the body is excluded.  I agree it would be cleaner
if the contract were just the generic formals, but in Ada that would
require a lot of additional information in the formals.

>> Also, the generic contract model applies only to compile-time rules.
>
> Sure, that is a contract model of the meta language of generics. If it were
> properly contracted generics produced only legal "Ada proper" programs.
>
>> The fact that the instance body is guaranteed to be legal doesn't
>> mean that it will work properly!
>
> Yes, the same applies to non-generic subprograms. Properly typed arguments
> do not guaranty it working. Legality does not imply correctness.
>
>> And there are a few cases where we
>> deliberately "cheat" in the RM, by making something raise an exception
>> in a generic, when it would normally be a legality rule.
>
> Conversion of errors into exceptions is an extremely bad idea. The same
> fault is represented by dynamic pre-/pos-conditions, assertions,
> accessibility checks, tag errors.

But it's not feasible to catch all errors statically.  If you made a
rule that all preconditions (for example) must be statically checked,
that would simply mean lots of preconditions are inexpressible.

I agree about accessibility checks -- I wish those were always static.

- Bob