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

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 23.11.11 14:30, Dmitry A. Kazakov wrote:

>>> So it is the debugging driven design you are advocating for. Designing by
>>> fixing bugs. Nice, very nice... exactly the thing I don't want for Ada.
>>
>> Specifications have bugs.
> 
> That is irrelevant to the discussion about designing programs. If you want
> to switch to designing specifications then what do run-time assertions have
> to do with that?

Run-time assertions will tell when there probably is something wrong
with any of: the specification; the program that should implement it;
the compiler; the hardware; ...


>>> One of the key points of good design is NOT to have such descriptions. The
>>> reader of the program, be it human or the compiler should be able to
>>> *understand* what you are describing.
>>
>> What is it that a reader of a package spec should be able to understand?
> 
> The package specification, I suppose.
> 
>> ADTs without invariants?
> 
> Invariant is an implementation detail

No, there is no implementation in a DbC contract. There is, however,
a contractual obligation that each instance of a DbC type establish,
at certain points, an invariant that its programmer has expressed
in terms of publicly visible "features" of the type. (Ideally, these
will be expressions involving idempotent functions).

The actual properties of implementations are not relevant to the DbC
client, only the properties expressed in the contract.


>> Subprograms of unknown effect,
> 
> You confuse interface and implementation.

I call a subprogram because it has an effect. Is this unusual?
In order to choose the right subprogram, I need to know its
effect.  There is very little that a subprogram profile tells
about the body's effect. By comparison, an ADT that specifies
preconditions, postconditions, and DbC-invariants, lets me know
more about what will be the case after the body has executed
successfully, or failed.

>>>> There is no right or wrong in most programs.
>>>
>>> You cannot build safe software on false premises.
>>
>> Almost all programs have a number of things that can go wrong,
> 
> Program code cannot GO wrong, it IS either wrong or not, here and now.

No, we don't know whether an executable program is right or wrong,
for almost all programs. We can detect that a run of a program
has a certain effect.
  From the effects, we tend to conclude that a program
has this or that property.  But in general, this is just as wrong,
we might see false positives, do not notice something that
someone else will later notice, or be wrong about diagnosing
right or wrong. But we have an issue, and look into it.
  If an executable program is not proven correct in all
possible ways, we simply do not know what it is.
We hope to have done our best, that's all.

"Doctor, something hurts!" seems less useful than
"Doctor, whenever I lift my left arm above the height
of my shoulders, I could scream!".