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

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

On 23.11.11 20:48, Dmitry A. Kazakov wrote:

>>>> 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.
>
> That is exactly why contracts cannot be dynamic. Dynamic means statically
> undecidable. How are you going to know anything about the subprogram, if
> that is unknown until run-time?

The typical example is a stack and its contract referring to
values available at runtime: from the contract, I learn that a stack
is initially empty and has a certain capacity. When there
is room (which is the case after object creation), I may push
an element on top of the stack.  From the postcondition of
`push`, I learn that the stack is not empty after the execution
of `push`. Not being empty is the precondition of `pop`. Hence,
the sequence
   create
   push
   pop
is safe in whichever implementation, provided the programmers
follow the contractual obligations.

Similarly, for Sqrt, Ada throws Argument_Error if the caller
fails to establish the implicit precondition of Sqrt: that
the argument must be an element of the domain of the corresponding
mathematical function. In this case, one might specify
   pre => (X >= 0.0)
where X is of type Float_Type'Base, Float_Type being the generic
formal.
I could learn something about the result of Sqrt from
its postcondition. Sometimes the postcondition can use
simpler functions to express the result that a programmer should
expect. But while Sqrt'Result * Sqrt'Result = X does not work (because
computers will not compute mathematical results in many cases),
expressing the other part of Sqrt's postcondition (LRM A.5.1(12))
is possible:

   post => (Sqrt'Result >= 0.0)

There are implementation requirements, too, so

   post => (if X = 0.0 then
               Sqrt'Result = 0.0
            elsif X = 1.0 then
                Sqrt'Result = 1.0
            else
                Sqrt'Result >= 0.0)

Is Sqrt'Result statically determinable? Statically useful?
I guess there is information in the postcondition that can be
used during development and also by source text analysis.
Should the postcondition give a maximal result in terms of
attributes of Float_Type'Base?
But certainly, if some Sqrt purports to implement the contract
and then a runtime check of the postcondition raises an exception,
this is an effect caused by not following the contract.
If the postcondition is correct, fix the implementation, then.

> One nice thing about inconsistencies is that they corrupt the whole system
> of reasoning. You cannot presume "for practical reason" that 2+2=5, because
> that will ruin everything else.

Ruin depends on the frame of reference.  There is good reason to
frown at first vis-�-vis the fact that 99 / 100 = 0.
A language design first needs to establish the rules by which
99 / 100 = 0. Only then one may study programs and say which
things make sense and which ones do not. Meyer's frames of
reference transcend the logic of just programs in several
dimensions, I think.  For illustration, he contrasts obligations
moving work between client and supplier and identifies
styles of DbC: if a subprogram is lenient and accepts everything,
it tends to deal with all cases. If a subprogram is demanding,
then only suitable values can be supplied and the implementation
is simpler, having lead to simpler systems. One may try either
style in some larger project and observe the outcome.



>>>>>> 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.
>
> It is not about anybody's knowledge. A program is correct or not
> independently on whether you or anybody else knows that.

"Is correct or not correct" sounds like a tautology and says just
as much. For any k in a numbering of programs P, all we can say is
that P(k) may be correct or not. We cannot say "P(k) is correct"
before studying P(k) and we also cannot say "P(k) is not correct"
before studying P(k).

Informally speaking, then, things can go wrong, because we know
only that the program is correct or not.