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

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

On 23.11.11 10:45, Yannick Duchêne (Hibou57) wrote:
> Le Wed, 23 Nov 2011 09:50:26 +0100, Georg Bauhaus <rm.dash-bauhaus@futureapps.de> a écrit:
>> `put`, in DbC, may fail when it tries to establish
>> the state of variables so that the postcondition is
>> true, for example, because of a hardware error.
>> Can this be attributed to an incomplete precondition,
>> though?
> Obviously not, but an incomplete pre-condition (lack of `not D.has (x)` in the Pre or lack in the Post of an `old D.has (x)` associated with the count), is not an hardware error. Cannot compare things of different nature.
>
> But don't bother, just noticed it because it was funny, no need to discuss this detail in deep, this would offer no meaningful value to the topic.
>

This is the best opportunity for some detail:
The precondition does not mention "not has(x)".
The dictionary may well have an entry for x,
but you can still add it and the postcondition
will be true:

    #Name    #Age
    Miller   56

d.put(x => 56, key => "Jones)

    #Name    #Age
    Miller   56
    Jones    56

In fact, `put` can replace Miller's age with another
Miller's age  and still the state is as pre/post say.
If `put` should not replace, this needs to be stated.
And then it should raise an exception.  Just like
Ada's containers do, except that DbC exceptions typically
have more information about what went wrong.