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

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

On 24.11.11 10:27, Dmitry A. Kazakov wrote:
> On Thu, 24 Nov 2011 08:07:45 +0000, Simon Wright wrote:
>
>> To take Georg's example of the stack, I don't see how you're going to
>> express the fact that its capacity is bounded other than by comments
>> about constraint errors or by preconditions.
>
> The point is that when this behavior can be expressed

I hate to go on when we have a summary by Stefan Lucks but two
more issues:
Maybe there isn't that much of a disagreement, if we can fake
the choice by replacing it with a choice of style; notably,
a project may require that
    pre => True
    post => May_Raise
be the only conditionals allowed.  Then, programmers of clients
should be ready to handle failures. This choice still doesn't
restrict Ada contracts to get all the flexibility of statically
checked expressions, but is closer to exceptions only, I'd think.


The notions are not ones of behavior, just like debugging
statements, but rather more simple, and specifically intended
to be only guiding the creation of behavioral aspects of the
program proper: Like in the example given in [1], programmers
are supposed to write bodies so that the conditionals given
in pre/post/inv are meaningful. This is their contractual obligation.
A precondition of the form T'Valid (Some_Input) is inappropriate
if the body doesn't actually implement its meaning, since
assertions do *not* count as program behavior. Note that I am
saying "they do not count", and not saying "they do not result
in behavior": it does not matter that in some circumstances
they are supposed to result in behavior, for example, during
testing.

The capacity of a stack can be a trivial Type_Invariant if the
size is a type constraint. There will be less silly scenarios
than these, but nevertheless:

procedure Stacking (N: Positive) is
    
    type T is (One, Two, Three);
    
    package Local_Stacks is
       
       type Stack (Capacity : Natural) is tagged private
           with Type_Invariant => (Stack.Capacity = N
                                   and True);  -- etc.

    private
       ...
    end Local_Stacks;
   
    package body Local_Stacks is separate;
   
    S1 : Local_Stacks.Stack (N);  -- o.K.
    S2 : Local_Stacks.Stack (42);
      -- raises when 42 /= N and pramga Assertion_Policy (Check);
begin
    null;
end Stacking;


> A dynamic precondition does not express anything,

Well, frankly, any expression demonstrably expresses something,
because an Ada compiler can and will assign meaning to all
constituent parts of the expression. The expression does not
necessarily have a Boolean value at compile time, but it
certainly isn't void of meaning. As per intent.
Programmers also assign meaning to expressions in assertions
of the contract.

> SPARK does it right, Eiffel and now Ada do it wrong.
>
> If correctness cannot be proved
> statically, then the requirement expressed by the precondition must be
> considered as not satisfied.

We may state our assumptions and have them checked, or we may
state our assumptions and perform the checks ourselves, before
runtime, statically.
Like when showing that for a stack object, the sequence
(not Is_Full, Push, Pop) is a safe sequence, ceteris paribus.
That is, safe in terms of the contract, ignoring hardware failures,
ignoring a breach of contract in the stack's bodies. Since,
normally, any of these can be true, one may prepare for failure.
But! There is no need for the sequence of calls to be changed
in order to handle failures! Is is a correct sequence.

This style just seems more expressive than "raise Constraint_Error"
without indication of possible causes, when some are in fact known,
and expressed as assertions, before compile time! I am not so sure that
programmers are fooling themselves into thinking that adding
descriptive assertions somehow makes a program automatically correct.
It only helps with this effort.

__
[1] http://www2.adacore.com/wp-content/uploads/2006/03/Ada2012_Rational_Introducion.pdf
Page 2, on the right.