Generic-Package Elaboration Question / Possible GNAT Bug.

Generic-Package Elaboration Question / Possible GNAT Bug.

[Shark8]

I was working on some simple little array manipulation functions when
I encountered an interesting behavior in the compiler; it said that
trying to instantiate a function of the form:
   Generic
      Type Element is Private;
      Type Index_Type is (<>);
      Type Array_Type is Array (Index_Type Range <>) of Element;
   Function Generic_Delete( Index : In Index_Type; Data : In
Array_Type ) Return Array_Type;

When given the following body, the compiler complained about the
Index_Range'First/Last not being static:

   Function Generic_Delete( Index : In Index_Type; Data : In
Array_Type ) Return Array_Type is
   begin
      if Index not in Data'Range then
         Raise Constraint_Error;
      else
           case Index is
           when Index_Type'First => Return
Data( Index_Type'Succ(Index)..Data'Last );
           when Index_Type'Last => Return
Data( Data'First..Index_Type'Pred(Index) );
           when others =>
                  Return Data( Data'First..Index_Type'Pred(Index) )
  		 & Data( Index_Type'Succ(Index)..Data'Last );
           end case;
      end if;
   end Generic_Delete;

Now, I know that the following works as a fix:

     Function Generic_Delete( Index : In Index_Type; Data : In
Array_Type ) Return Array_Type is
     begin
        if Index not in Data'Range then
           Raise Constraint_Error;
        else
           if Index = Data'First then
              Return Data( Index_Type'Succ(Index)..Data'Last );
           elsif Index = Data'Last then
              Return Data( Data'First..Index_Type'Pred(Index) );
           else
              Return Data( Data'First..Index_Type'Pred(Index) )
  		 & Data( Index_Type'Succ(Index)..Data'Last );
           end if;
        end if;
     end Generic_Delete;

But the question that came to my mind after reading the ARM section on
the error (sorry, I forgot to write it down) is, why is it not static?
Is it because though the elaboration-parameters *may* be known [and
static] at compile-time that some instantiation might NOT be
[guaranteed] to be known at compile-time? (i.e. because the compiler
cannot guarantee that you won't throw 1..N where N is something pulled
from the user-input?)

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

[Robert A Duff]

Shark8 <onewingedshark@gmail.com> writes:

> I was working on some simple little array manipulation functions when
> I encountered an interesting behavior in the compiler; it said that
> trying to instantiate a function of the form:
>    Generic
>       Type Element is Private;
>       Type Index_Type is (<>);
>       Type Array_Type is Array (Index_Type Range <>) of Element;
...
> But the question that came to my mind after reading the ARM section on
> the error (sorry, I forgot to write it down) is, why is it not static?

Generic formals are not static, because that would violate the generic
contract model.  That is, the compiler should be able to determine the
legality of the generic body without knowing anything about any
instantiations.

In your case statement, what if the range of Index_Type were 1..1?
Then 'First = 'Last, so there's a duplicate in your case statement
(which would be illegal in the instance, but we're not supposed to
know about the instance).

In general, the design of Ada is that if a generic body is legal,
then every possible instance is legal (so the compiler need not
check the instances).  The design of C++ templates is very different
in this regard!

> Is it because though the elaboration-parameters *may* be known [and
> static] at compile-time that some instantiation might NOT be
> [guaranteed] to be known at compile-time? (i.e. because the compiler
> cannot guarantee that you won't throw 1..N where N is something pulled
> from the user-input?)

Yeah, that's another example.

By the way, I suggest:

    type Index_Type is range <>;

Unconstrained arrays don't make a whole lot of sense when the index
type is enumeration or modular.

And if you add some assertions, to require that Index_Type'First >
Index_Type'Base'First, and Data'First = Index_Type'First, then
you can simplify your code -- you won't need the case statement.

Well, maybe you also need to assert that Data'Last < Index_Type'Base'Last.

Consider using Ada 2012 preconditions and/or predicates.

- Bob

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

[Shark8]

On Nov 19, 4:12 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> Shark8 <onewingedsh...@gmail.com> writes:
> > I was working on some simple little array manipulation functions when
> > I encountered an interesting behavior in the compiler; it said that
> > trying to instantiate a function of the form:
> >    Generic
> >       Type Element is Private;
> >       Type Index_Type is (<>);
> >       Type Array_Type is Array (Index_Type Range <>) of Element;
> ...
> > But the question that came to my mind after reading the ARM section on
> > the error (sorry, I forgot to write it down) is, why is it not static?
>
> Generic formals are not static, because that would violate the generic
> contract model.  That is, the compiler should be able to determine the
> legality of the generic body without knowing anything about any
> instantiations.
>
> In your case statement, what if the range of Index_Type were 1..1?
> Then 'First = 'Last, so there's a duplicate in your case statement
> (which would be illegal in the instance, but we're not supposed to
> know about the instance).

Oh, good point! I hadn't even considered that.

> In general, the design of Ada is that if a generic body is legal,
> then every possible instance is legal (so the compiler need not
> check the instances).  The design of C++ templates is very different
> in this regard!

*nod* -- I understand that Ada's generics are quite different than C+
+'s templates. Some of the reasons I've come across make a whole lot
more sense to me for the Ada model than the C++, this "every possible
instance" restriction is one such case. Who would want a system where
a 'general' feature only worked for *some* instances. {Meaning the
general feature wasn't actually .}

> By the way, I suggest:
>
>     type Index_Type is range <>;
>
> Unconstrained arrays don't make a whole lot of sense when the index
> type is enumeration or modular.
>
> And if you add some assertions, to require that Index_Type'First >
> Index_Type'Base'First, and Data'First = Index_Type'First, then
> you can simplify your code -- you won't need the case statement.
>
> Well, maybe you also need to assert that Data'Last < Index_Type'Base'Last.
>
> Consider using Ada 2012 preconditions and/or predicates.
>
> - Bob

I'm looking forward to the Ada 2012 version, though as this post
indicates I still have a bit of a way to go to really *understand*
even the base of the language; I'm enjoying 'playing' with the
language, though the slow-going on getting that fuller understanding
can be frustrating. (I'm still a complete 'noob' when it comes to
tasking, though that's one of the more intriguing portions of the
language.)

Thanks for the help/reply.

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

[Dmitry A. Kazakov]

On Sat, 19 Nov 2011 15:36:33 -0800 (PST), Shark8 wrote:

> On Nov 19, 4:12�pm, Robert A Duff <bobd...@shell01.TheWorld.com>
> wrote:

>> In general, the design of Ada is that if a generic body is legal,
>> then every possible instance is legal (so the compiler need not
>> check the instances). �The design of C++ templates is very different
>> in this regard!
> 
> *nod* -- I understand that Ada's generics are quite different than C+
> +'s templates. Some of the reasons I've come across make a whole lot
> more sense to me for the Ada model than the C++, this "every possible
> instance" restriction is one such case. Who would want a system where
> a 'general' feature only worked for *some* instances. {Meaning the
> general feature wasn't actually .}

I don't know if Ada keeps that promise for generic bodies, but it certainly
does not for the specifications. Generic contracts are too weak for that.
Example:

generic
   type T is tagged private;
package Legal is
   type S is new T with null record;
   not overriding procedure Foo (X : in out S);
end Legal;

This and the body would successfully compile ignoring the fact that there
might exist tagged types with a primitive operation named Foo.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[AdaMagica]

On 20 Nov., 10:55, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> > On Nov 19, 4:12 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
> > wrote:
> >> In general, the design of Ada is that if a generic body is legal,
> >> then every possible instance is legal (so the compiler need not
> >> check the instances).  The design of C++ templates is very different
> >> in this regard!
>
> I don't know if Ada keeps that promise for generic bodies, but it certainly
> does not for the specifications. Generic contracts are too weak for that.
> Example:
>
> generic
>    type T is tagged private;
> package Legal is
>    type S is new T with null record;
>    not overriding procedure Foo (X : in out S);
> end Legal;
>
> This and the body would successfully compile ignoring the fact that there
> might exist tagged types with a primitive operation named Foo.

Note that Bob said this holds true for *bodies*, here you have a
*spec* that might produce an illegal instance.

For bodies, Ada always assumes the worst.

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

[Dmitry A. Kazakov]

On Sun, 20 Nov 2011 23:25:39 -0800 (PST), AdaMagica wrote:

> On 20 Nov., 10:55, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>>> On Nov 19, 4:12�pm, Robert A Duff <bobd...@shell01.TheWorld.com>
>>> wrote:
>>>> In general, the design of Ada is that if a generic body is legal,
>>>> then every possible instance is legal (so the compiler need not
>>>> check the instances). �The design of C++ templates is very different
>>>> in this regard!
>>
>> I don't know if Ada keeps that promise for generic bodies, but it certainly
>> does not for the specifications. Generic contracts are too weak for that.
>> Example:
>>
>> generic
>> � �type T is tagged private;
>> package Legal is
>> � �type S is new T with null record;
>> � �not overriding procedure Foo (X : in out S);
>> end Legal;
>>
>> This and the body would successfully compile ignoring the fact that there
>> might exist tagged types with a primitive operation named Foo.
> 
> Note that Bob said this holds true for *bodies*, here you have a
> *spec* that might produce an illegal instance.

If the specification becomes illegal so does the body. 

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[AdaMagica]

On 21 Nov., 09:43, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> If the specification becomes illegal so does the body.

So what?
If the instance of the spec is legal, so is the body - that's all that
was said, in contrast to C++: The compiler (and the programmer) does
not need to look into the body to decide whether the instantiation is
legal.

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

[Robert A Duff]

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

> On Sun, 20 Nov 2011 23:25:39 -0800 (PST), AdaMagica wrote:
>
>> On 20 Nov., 10:55, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
>> wrote:
>>>> On Nov 19, 4:12�pm, Robert A Duff <bobd...@shell01.TheWorld.com>
>>>> wrote:
>>>>> In general, the design of Ada is that if a generic body is legal,
>>>>> then every possible instance is legal (so the compiler need not
>>>>> check the instances). �The design of C++ templates is very different
>>>>> in this regard!
>>>
>>> I don't know if Ada keeps that promise for generic bodies, ...

I think it does.  I'd be interested in any counterexamples.
(Implementation defined cases don't count.)

>...but it certainly
>>> does not for the specifications.

Right.

>...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".

Also, the generic contract model applies only to compile-time rules.
The fact that the instance body is guaranteed to be legal doesn't
mean that it will work properly!  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.

>> Note that Bob said this holds true for *bodies*, here you have a
>> *spec* that might produce an illegal instance.
>
> If the specification becomes illegal so does the body. 

OK, but my comment was the other way around:  "if a generic body is
legal, then ..."

- Bob

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

[Dmitry A. Kazakov]

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.

>>...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.

> 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.
 
-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Adam Beneschan]

On Nov 19, 1:14 pm, Shark8 <onewingedsh...@gmail.com> wrote:
> I was working on some simple little array manipulation functions when
> I encountered an interesting behavior in the compiler; it said that
> trying to instantiate a function of the form:
>    Generic
>       Type Element is Private;
>       Type Index_Type is (<>);
>       Type Array_Type is Array (Index_Type Range <>) of Element;
>    Function Generic_Delete( Index : In Index_Type; Data : In
> Array_Type ) Return Array_Type;
>
> When given the following body, the compiler complained about the
> Index_Range'First/Last not being static:
>
>    Function Generic_Delete( Index : In Index_Type; Data : In
> Array_Type ) Return Array_Type is
>    begin
>       if Index not in Data'Range then
>          Raise Constraint_Error;
>       else
>            case Index is
>            when Index_Type'First => Return
> Data( Index_Type'Succ(Index)..Data'Last );
>            when Index_Type'Last => Return
> Data( Data'First..Index_Type'Pred(Index) );
>            when others =>
>                   Return Data( Data'First..Index_Type'Pred(Index) )
>                  & Data( Index_Type'Succ(Index)..Data'Last );
>            end case;
>       end if;
>    end Generic_Delete;
>
> Now, I know that the following works as a fix:
>
>      Function Generic_Delete( Index : In Index_Type; Data : In
> Array_Type ) Return Array_Type is
>      begin
>         if Index not in Data'Range then
>            Raise Constraint_Error;
>         else
>            if Index = Data'First then
>               Return Data( Index_Type'Succ(Index)..Data'Last );
>            elsif Index = Data'Last then
>               Return Data( Data'First..Index_Type'Pred(Index) );
>            else
>               Return Data( Data'First..Index_Type'Pred(Index) )
>                  & Data( Index_Type'Succ(Index)..Data'Last );
>            end if;
>         end if;
>      end Generic_Delete;
>
> But the question that came to my mind after reading the ARM section on
> the error (sorry, I forgot to write it down) is, why is it not static?
> Is it because though the elaboration-parameters *may* be known [and
> static] at compile-time that some instantiation might NOT be
> [guaranteed] to be known at compile-time? (i.e. because the compiler
> cannot guarantee that you won't throw 1..N where N is something pulled
> from the user-input?)

I think one thing to keep in mind is that it's legal in Ada to compile
the specification of a generic, and *then* compile one or more
instances of the generic, before the generic body is ever seen.  So
say you compile source S1 containing the specification of
Generic_Delete, and then compile source S2 which instantiates
Generic_Delete with Index_Type => Some_Subtype where Some_Subtype has
a non-static bound (like your 1..N).  Later, you compile source S3
containing the body of Generic_Delete.  If the CASE statement you
wrote were legal, it would make source S2 illegal retroactively, which
isn't really feasible.  I think that's one reason, perhaps the main
reason, why the Ada rules are written the way they are---a generic
body has to be legal for all possible instantiations for which the
specification is legal.

                          -- Adam

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

[Robert A Duff]

"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

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

[J-P. Rosen]

Le 21/11/2011 14:50, Dmitry A. Kazakov a �crit :
> 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.
>  
Sure. If you have a better idea (short of redesigning the whole language
or making unacceptable upward incompatibilities), I'm sure the ARG would
be deligthed to hear. We discussed the issues ad nauseum and could not
find any other solution.

-- 
---------------------------------------------------------
           J-P. Rosen (rosen@adalog.fr)
Adalog a d�m�nag� / Adalog has moved:
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00

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

[Dmitry A. Kazakov]

On Mon, 21 Nov 2011 14:41:05 -0500, Robert A Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> 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.

It is same as to say that it is infeasible to determine program legality
statically. Legality is static per definition.

> If you made a
> rule that all preconditions (for example) must be statically checked,
> that would simply mean lots of preconditions are inexpressible.

If a "precondition" is not static then it is just a part of the *code*
determining the control flow. In earlier times such things were called
prologue and epilogue. There are many issues with them:

1. Stuffing declarative regions with executable code;
2. Defeating principles of structured programming: non-local control flow;
3. Ignoring separation of implementation and interface.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Dmitry A. Kazakov]

On Mon, 21 Nov 2011 21:40:30 +0100, J-P. Rosen wrote:

> Le 21/11/2011 14:50, Dmitry A. Kazakov a �crit :
>> 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.
>>  
> Sure. If you have a better idea (short of redesigning the whole language
> or making unacceptable upward incompatibilities), I'm sure the ARG would
> be deligthed to hear. We discussed the issues ad nauseum and could not
> find any other solution.

Hmm, if pre-/post-conditions were a solution, what was the problem?

Regarding run-time exceptions, these are not errors, they are a part of
program's behavior. I think that a solution is not in adding new sources of
exceptions, but by making exceptions contracted (using conditional
contracts, e.g. "I don't raise, if you don't", "I don't raise if there is N
units of memory free" etc).

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Georg Bauhaus]

On 22.11.11 09:29, Dmitry A. Kazakov wrote:
>  I think that a solution is not in adding new sources of
> exceptions, but by making exceptions contracted (using conditional
> contracts, e.g. "I don't raise, if you don't", "I don't raise if there is N
> units of memory free" etc).

I think that, with the exception of compiler-determines-all-of-this,
the above is a well known characterization of DbC.

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

[Dmitry A. Kazakov]

On Tue, 22 Nov 2011 11:25:59 +0100, Georg Bauhaus wrote:

> On 22.11.11 09:29, Dmitry A. Kazakov wrote:
>>  I think that a solution is not in adding new sources of
>> exceptions, but by making exceptions contracted (using conditional
>> contracts, e.g. "I don't raise, if you don't", "I don't raise if there is N
>> units of memory free" etc).
> 
> I think that, with the exception of compiler-determines-all-of-this,
> the above is a well known characterization of DbC.

Not really. DbC is about upfront formalized requirements.

For contracted exceptions more important is how contracts influence the
implementation. The idea is that in order to be legal the program must be
written so that the contract would be provable. If not provable, either the
program or the contract has to be changed. That is opposite to dynamic
checks, you don't need to check for non-contracted exceptions.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Georg Bauhaus]

On 22.11.11 15:32, Dmitry A. Kazakov wrote:
> On Tue, 22 Nov 2011 11:25:59 +0100, Georg Bauhaus wrote:
> 
>> On 22.11.11 09:29, Dmitry A. Kazakov wrote:
>>>  I think that a solution is not in adding new sources of
>>> exceptions, but by making exceptions contracted (using conditional
>>> contracts, e.g. "I don't raise, if you don't", "I don't raise if there is N
>>> units of memory free" etc).
>>
>> I think that, with the exception of compiler-determines-all-of-this,
>> the above is a well known characterization of DbC.
> 
> Not really. DbC is about upfront formalized requirements.

Not sure, are you speaking about DbC (TM)?

> For contracted exceptions more important is how contracts influence the
> implementation. The idea is that in order to be legal the program must be
> written so that the contract would be provable. If not provable, either the
> program or the contract has to be changed. That is opposite to dynamic
> checks, you don't need to check for non-contracted exceptions.

DbC (TM) is meant to be

(a) A model of design: client-ensures-proconditions and then
    supplier-ensures-postconditions, so as to keep certain properties
    of the object invariant.

(b) A debugging ("design", "specification", bla-bla) aid leading
    towards formally proven components where such proofs are possible.

"An exception is the element's inability to fulfil its contract, for any
reason: a hardware failure has occurred, a called routine has failed, a
software bug makes it impossible to satisfy the contract."
Meaningful responses: retrying after adjustments, organized panic,
false alarm.[1]

Without those dynamic checks, we wouldn't ever notice a failure?
Assuming, in this case, that there is still some amount of software
whose behavior is not known until it executes.


__
[1] http://www.eiffel.com/developers/design_by_contract_in_detail.html

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

[Dmitry A. Kazakov]

On Tue, 22 Nov 2011 16:02:06 +0100, Georg Bauhaus wrote:

> On 22.11.11 15:32, Dmitry A. Kazakov wrote:
>> On Tue, 22 Nov 2011 11:25:59 +0100, Georg Bauhaus wrote:
>> 
>>> On 22.11.11 09:29, Dmitry A. Kazakov wrote:
>>>>  I think that a solution is not in adding new sources of
>>>> exceptions, but by making exceptions contracted (using conditional
>>>> contracts, e.g. "I don't raise, if you don't", "I don't raise if there is N
>>>> units of memory free" etc).
>>>
>>> I think that, with the exception of compiler-determines-all-of-this,
>>> the above is a well known characterization of DbC.
>> 
>> Not really. DbC is about upfront formalized requirements.
> 
> Not sure, are you speaking about DbC (TM)?

I don't care about trade marks and definitions given by reference
manuals...

>> For contracted exceptions more important is how contracts influence the
>> implementation. The idea is that in order to be legal the program must be
>> written so that the contract would be provable. If not provable, either the
>> program or the contract has to be changed. That is opposite to dynamic
>> checks, you don't need to check for non-contracted exceptions.
> 
> DbC (TM) is meant to be
> 
> (a) A model of design: client-ensures-proconditions and then
>     supplier-ensures-postconditions, so as to keep certain properties
>     of the object invariant.

This is not a model of design, this a description of some contract.

The model of design is, for example, that components can be designed
independently when contracts are stated upfront.

> (b) A debugging ("design", "specification", bla-bla) aid leading
>     towards formally proven components where such proofs are possible.

I cannot decipher this, sorry.

> "An exception is the element's inability to fulfil its contract, for any
> reason: a hardware failure has occurred, a called routine has failed, a
> software bug makes it impossible to satisfy the contract."

An exception is a program state. It is not an inability. The behavior in an
exceptional state is contracted, at least in Ada it is.

> Without those dynamic checks, we wouldn't ever notice a failure?

How would you notice a failure to notice? No need to repeat it again and
again: dynamic checks of correctness are inconsistent, see the liar paradox
et al. Dynamic check is a part of program, which determines the program's
behavior. No more, no less.

> Assuming, in this case, that there is still some amount of software
> whose behavior is not known until it executes.

The software which behavior is unknown shall never be executed.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Georg Bauhaus]

On 22.11.11 17:23, Dmitry A. Kazakov wrote:

>> Not sure, are you speaking about DbC (TM)?
> 
> I don't care about trade marks and definitions given by reference
> manuals...

Frankly, doing so in some way will help discussing things.

DbC is ...
>> (b) A debugging ("design", "specification", bla-bla) aid leading
>>     towards formally proven components where such proofs are possible.
> 
> I cannot decipher this, sorry.

Meyer: "Programming is a human activity".
Programmers are led towards a solution during the process of programming.
Depending on the characteristics of the process, then,
programmers will produce different results.
DbC (TM), as a characteristic of a process, leads to products
that lend themselves to proving them correct more than others,
provided this is possible.


>> "An exception is the element's inability to fulfil its contract, for any
>> reason: a hardware failure has occurred, a called routine has failed, a
>> software bug makes it impossible to satisfy the contract."
> 
> An exception is a program state. It is not an inability. The behavior in an
> exceptional state is contracted, at least in Ada it is.

OK, erroneous execution. A program's behavior according to the contract.
Yes. But lame.


>> Without those dynamic checks, we wouldn't ever notice a failure?
> 
> How would you notice a failure to notice?

Really does not matter. There is no need to require forall-qualification
of every aspect of DbC(TM) when it is not meant to be in a program
if and only if the program (including hardware) is proven to be
100% such-and-such.  Impractical.

> The software which behavior is unknown shall never be executed.

But this is impossible, in general!

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

[Dmitry A. Kazakov]

On Tue, 22 Nov 2011 18:46:02 +0100, Georg Bauhaus wrote:

> On 22.11.11 17:23, Dmitry A. Kazakov wrote:
> 
>>> Not sure, are you speaking about DbC (TM)?
>> 
>> I don't care about trade marks and definitions given by reference
>> manuals...
> 
> Frankly, doing so in some way will help discussing things.

Any discussion should be based on the meaning of words.

Discussions about words are uninteresting to me.

>>> (b) A debugging ("design", "specification", bla-bla) aid leading
>>>     towards formally proven components where such proofs are possible.
>> 
>> I cannot decipher this, sorry.
> 
> Meyer: "Programming is a human activity".
> Programmers are led towards a solution during the process of programming.
> Depending on the characteristics of the process, then,
> programmers will produce different results.

I see no word "debugging" there.

> DbC (TM), as a characteristic of a process, leads to products
> that lend themselves to proving them correct more than others,
> provided this is possible.

I suppose drinking coffee does that as well. CDD [caffeine driven design]
(TM). As for randomly raised exceptions from dynamic checks, I doubt that
leads to better products. I my experience at least 40% of my debugging
efforts in Ada 95 was spent on catching accessibility checks faults. Ada
2005 improved that greatly. To me this is a vivid example why dynamic
checks are evil.

>>> "An exception is the element's inability to fulfil its contract, for any
>>> reason: a hardware failure has occurred, a called routine has failed, a
>>> software bug makes it impossible to satisfy the contract."
>> 
>> An exception is a program state. It is not an inability. The behavior in an
>> exceptional state is contracted, at least in Ada it is.
> 
> OK, erroneous execution.

If the program has a bug its execution is erroneous. Is it what you want to
say? So?

>>> Without those dynamic checks, we wouldn't ever notice a failure?
>> 
>> How would you notice a failure to notice?
> 
> Really does not matter. There is no need to require forall-qualification
> of every aspect of DbC(TM) when it is not meant to be in a program
> if and only if the program (including hardware) is proven to be
> 100% such-and-such.  Impractical.

Which then? You have to specify the failures you are going to notice. Once
you do qualify them, you would easily be able to avoid them. Note that all
the buzz is about noticing something unanticipated. That is impossible,
period. Anticipated failures are not bugs, they are states.

>> The software which behavior is unknown shall never be executed.
> 
> But this is impossible, in general!

I see the point, since it is impossible do right, you are going to do it
wrong. I am not arguing for or against your or Meyer's motivations. I only
state that it is wrong. 

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net...
 > I my experience at least 40% of my debugging
> efforts in Ada 95 was spent on catching accessibility checks faults. Ada
> 2005 improved that greatly. To me this is a vivid example why dynamic
> checks are evil.

It's not "dynamic checks" that are evil, it is checking the uncheckable that 
is evil. 95% of accessibility check failures (static or dynamic) have no 
correlation to any error, so they are just crying wolf. "Checks" that don't 
prevent errors are evil, period -- it doesn't matter how they are checked.

Note that I no longer even try to deal with accessibility checks; I use 
'Unchecked_Access (only). Indeed, I've only found one single instance in my 
code (since Ada 95, about 15 years now) where I could actually use 'Access 
without error. In all other cases, my code either needs '[Unchecked_]Access 
for some short-lived thing (like a call to a C API) which has long-lived 
types (because it is declared at library-level), or I have to manage the 
lifetime issues myself (using controlled types).

OTOH, dynamic checks like overflow checks and index checks are not evil, or 
maybe it would be better to say that they are the lesser of evils (getting 
the wrong answer silently is a greater evil). I don't see a practical 
alternative (proving a multiply does not overflow is difficult to do in 
general; I gave up trying in the Janus/Ada optimizer and simply try the 
operation to see what happens. It's not ideal, but it is the only practical 
solution).

                                Randy.

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

[Dmitry A. Kazakov]

On Tue, 22 Nov 2011 15:03:52 -0600, Randy Brukardt wrote:

> Note that I no longer even try to deal with accessibility checks; I use 
> 'Unchecked_Access (only).

Same with me, but since Ada 2005 I tend to use 'Access again, because it
works so much better in Ada 2005.

> OTOH, dynamic checks like overflow checks and index checks are not evil,

Sure, I meant only dynamic checks of *program correctness*. Overflow or
index are not such checks, they are here to enforce defined, contracted
behavior.

Pre-/post-conditions and accessibility checks pretend [only pretend] to be
correctness checks, yielding true if the program is correct. As the result
the user expects them not to raise exceptions and is programming the rest
correspondingly. That is a wrong idea, which makes programs less safe due
to false expectations. It is same as reading file and expecting that
End_Error is never raised. I want that exception expectations were
contracted and checked statically. If impossible to prove, the program
should only be legal if it is *visibly* annotated as potentially raising
the corresponding exception.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Georg Bauhaus]

On 22.11.11 20:15, Dmitry A. Kazakov wrote:

>> Meyer: "Programming is a human activity".
>> Programmers are led towards a solution during the process of programming.
>> Depending on the characteristics of the process, then,
>> programmers will produce different results.
>
> I see no word "debugging" there.

A debugging aid is a means of finding mistakes when developing programs.
Trying to write assertions pre/post/inv for types and their primitive operations
is a means of finding mistakes (bugs) at a number of stages during program
development. At one stage, I will state the intended effect of operations
on visible object state. At another stage, I might want to know why a
subprogram has failed to establish its postcondition and raised.
Answering the questions revolves around the very same subject.
(It will be cool to make "permissible input" to a subprogram a consequence
of 'Valid; is it practical?)

Then, evaluation of the conditionals may or may not happen (depending on
settings like Assertion_Policy). The intent is to prod programmers into trying
harder with one specific goal: to render the conditionals a *consequence*
of the program (without assertions), a redundancy, rather than a part
of it.  A non-trivial consequence that reflects the intent. A non-trivial
consequence of a suitable corrected program.
When this is achieved, assertions not only will not negatively affect any
execution of the program, they also document programmers' intent which
is otherwise lost in mere implications, obscure comments, unspoken.

>
>> DbC (TM), as a characteristic of a process, leads to products
>> that lend themselves to proving them correct more than others,
>> provided this is possible.
>
> I suppose drinking coffee does that as well.

No, coffee is not known to yield better manifestations of intended
subprogram behavior in source text, certainly not better than specifying
conditions (program states) framing possible executions.  Coffee can have
rather obfuscating long term effects, in particular when spilt.


> I my experience at least 40% of my debugging
> efforts in Ada 95 was spent on catching accessibility checks faults. Ada
> 2005 improved that greatly. To me this is a vivid example why dynamic
> checks are evil.

One may prefer static checks and still want dynamic checks for
cases where static checks are not within reach of any tool
known to man.


> You have to specify the failures you are going to notice.

DbC (TM) suggests that you specify the set of states
that a program can reach if both the program

(a) is started from some state in a set of given states and

(b) if all goes well.

You do not specify what happens if not both (a) and (b).

(Hence,  trying alternatives, organized panic, or hoping for
false alarm if not both (a) and (b). Rescue clauses are a
there to assist the brave only.)

> Once
> you do qualify them, you would easily be able to avoid them.

Yes.

> Note that all
> the buzz is about noticing something unanticipated.

If a description of possible program states in not exhaustive,
then, nevertheless, this description establishes a non-empty set
of states, and another non-empty set, its complement.
When a state is found to be in the complement,
then I'd like to know this, even when this knowledge just teaches me
that my original attempt at specifying conditions was wrong.
I'm told by way of an exception raised.

>>> The software which behavior is unknown shall never be executed.
>>
>> But this is impossible, in general!
>
> I see the point, since it is impossible do right, you are going to do it
> wrong. I am not arguing for or against your or Meyer's motivations. I only
> state that it is wrong.

You do use compilers, and since it is impossible to know their behavior in
general, are you doing wrong?

There is no right or wrong in most programs. There is only I/O
that satisfies users. I can try to do it right, locally.
I'll try to make programs as good as possible.
As part of this effort, I can state my expectations of how the
subprograms should behave. This may be universally wrong,
improved types might be better, but should I do nothing because
something is wrong in principle?  At least I'm not allowed to
follow that path because of deadlines. :-)

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

[Georg Bauhaus]

On 22.11.11 22:26, Dmitry A. Kazakov wrote:

> Sure, I meant only dynamic checks of *program correctness*. Overflow or
> index are not such checks, they are here to enforce defined, contracted
> behavior.
>
> Pre-/post-conditions and accessibility checks pretend [only pretend] to be
> correctness checks, yielding true if the program is correct. As the result
> the user expects them not to raise exceptions

This will indeed be a wrong expectation; why would programmers
expect that there will be no exceptions if there are checks
all over the place?

> and is programming the rest
> correspondingly. That is a wrong idea, which makes programs less safe due
> to false expectations. It is same as reading file and expecting that
> End_Error is never raised. I want that exception expectations were
> contracted and checked statically. If impossible to prove, the program
> should only be legal if it is *visibly* annotated as potentially raising
> the corresponding exception.

DbC (TM) means: an objects primitive operation may raise an exception.
That's part of the business.

Thus if there is

    procedure ...
       with post => postcondition;

then, yes, it should probably be understood to mean

    procedure ...
       with post => raise when not postcondition;

is there substantial difference in behavior, regarding both that
of the program and that of the programmer?

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

[Yannick Duchêne (Hibou57)]

A guess attempt: does not depend on Generic_Delete implementation, but  
rather on a Generic_Delete instantiation parameters. If you could post the  
instantiation snippet too… (with declarations it depends on).

Le Sat, 19 Nov 2011 22:14:44 +0100, Shark8 <onewingedshark@gmail.com> a  
écrit:

> I was working on some simple little array manipulation functions when
> I encountered an interesting behavior in the compiler; it said that
> trying to instantiate a function of the form:
>    Generic
>       Type Element is Private;
>       Type Index_Type is (<>);
>       Type Array_Type is Array (Index_Type Range <>) of Element;
>    Function Generic_Delete( Index : In Index_Type; Data : In
> Array_Type ) Return Array_Type;
>
> When given the following body, the compiler complained about the
> Index_Range'First/Last not being static:
>
>    Function Generic_Delete( Index : In Index_Type; Data : In
> Array_Type ) Return Array_Type is
>    begin
>       if Index not in Data'Range then
>          Raise Constraint_Error;
>       else
>            case Index is
>            when Index_Type'First => Return
> Data( Index_Type'Succ(Index)..Data'Last );
>            when Index_Type'Last => Return
> Data( Data'First..Index_Type'Pred(Index) );
>            when others =>
>                   Return Data( Data'First..Index_Type'Pred(Index) )
>   		 & Data( Index_Type'Succ(Index)..Data'Last );
>            end case;
>       end if;
>    end Generic_Delete;
>
> Now, I know that the following works as a fix:
>
>      Function Generic_Delete( Index : In Index_Type; Data : In
> Array_Type ) Return Array_Type is
>      begin
>         if Index not in Data'Range then
>            Raise Constraint_Error;
>         else
>            if Index = Data'First then
>               Return Data( Index_Type'Succ(Index)..Data'Last );
>            elsif Index = Data'Last then
>               Return Data( Data'First..Index_Type'Pred(Index) );
>            else
>               Return Data( Data'First..Index_Type'Pred(Index) )
>   		 & Data( Index_Type'Succ(Index)..Data'Last );
>            end if;
>         end if;
>      end Generic_Delete;
>
> But the question that came to my mind after reading the ARM section on
> the error (sorry, I forgot to write it down) is, why is it not static?
> Is it because though the elaboration-parameters *may* be known [and
> static] at compile-time that some instantiation might NOT be
> [guaranteed] to be known at compile-time? (i.e. because the compiler
> cannot guarantee that you won't throw 1..N where N is something pulled
> from the user-input?)


-- 
“Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on  
Programming — Alan J. — P. Yale University]
“Structured Programming supports the law of the excluded muddle.” [Idem]

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

[Yannick Duchêne (Hibou57)]

Le Mon, 21 Nov 2011 14:08:04 +0100, Robert A Duff  
<bobduff@shell01.theworld.com> a écrit:
> 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.
Please, an example! :)

-- 
“Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on  
Programming — Alan J. — P. Yale University]
“Structured Programming supports the law of the excluded muddle.” [Idem]

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

[Yannick Duchêne (Hibou57)]

Le Tue, 22 Nov 2011 16:02:06 +0100, Georg Bauhaus  
<rm.dash-bauhaus@futureapps.de> a écrit:
> [1] http://www.eiffel.com/developers/design_by_contract_in_detail.html
Oops, not good for its claims, an exemple DbC™ use case in this page is  
erroneous:

> it will look as follows in Eiffel syntax, as part of a genericclass  
> DICTIONARY [ELEMENT]:
>
> put (x: ELEMENT; key: STRING) is
> 		-- Insert x so that it will be retrievable through key.
> 	require
> 		count <= capacity
> 		not key.empty
> 	do
> 		... Some insertion algorithm ...
> 	ensure
> 		has (x)
> 		item (key) = x		count = old count + 1
> 	end
The post-condition may fails, while the pre-condition was fulfilled  
(unless class DICTIONARY is weird). At least, a good candidate for a  
legitimate exception raise :p

-- 
“Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on  
Programming — Alan J. — P. Yale University]
“Structured Programming supports the law of the excluded muddle.” [Idem]

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

[Yannick Duchêne (Hibou57)]

Le Tue, 22 Nov 2011 22:03:52 +0100, Randy Brukardt <randy@rrsoftware.com>  
a écrit:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:12hfiflyf7pr5$.l3pkpgoid8xt$.dlg@40tude.net...
>  > I my experience at least 40% of my debugging
>> efforts in Ada 95 was spent on catching accessibility checks faults. Ada
>> 2005 improved that greatly. To me this is a vivid example why dynamic
>> checks are evil.
>
> It's not "dynamic checks" that are evil, it is checking the uncheckable  
> that is evil.
That's why C/C++ assertion macros will never value as much: it does not  
even  help to warrant the check, at the time it is done, is valid (just  
forget a hand written assertion check on array bounds, and the later hand  
written assertion check on the value of an item in that array will just be  
random result, and may even fail to trap an error).

I like the view you underline, that not only checks are to prevent invalid  
execution, but also have to ensure checks them-self are valid. Each check  
also warrant the validity of all other checks. In practice, this is more  
safely achieved automatically. Nice point.

-- 
“Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on  
Programming — Alan J. — P. Yale University]
“Structured Programming supports the law of the excluded muddle.” [Idem]

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

[Yannick Duchêne (Hibou57)]

Le Tue, 22 Nov 2011 22:03:52 +0100, Randy Brukardt <randy@rrsoftware.com>  
a écrit:
> Note that I no longer even try to deal with accessibility checks; I use
> 'Unchecked_Access (only). Indeed, I've only found one single instance in  
> my code (since Ada 95, about 15 years now) where I could actually use  
> 'Access without error. In all other cases, my code either needs  
> '[Unchecked_]Access for some short-lived thing (like a call to a C API)  
> which
> has long-lived types (because it is declared at library-level),
But you are loosing some expressiveness, don't you ?


-- 
“Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on  
Programming — Alan J. — P. Yale University]
“Structured Programming supports the law of the excluded muddle.” [Idem]

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

[Dmitry A. Kazakov]

On Wed, 23 Nov 2011 01:07:25 +0100, Georg Bauhaus wrote:

> Thus if there is
> 
>     procedure ...
>        with post => postcondition;
> 
> then, yes, it should probably be understood to mean
> 
>     procedure ...
>        with post => raise when not postcondition;
> 
> is there substantial difference in behavior, regarding both that
> of the program and that of the programmer?

It is lousy language design placing implementation (executable code
ensuring the desired behavior, e.g. raising exception) into declarations.
The proper one is:

   procedure ...
      raise Contraint_Error; -- I don't tell you when and how

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Georg Bauhaus]

On 23.11.11 04:49, Yannick Duchêne (Hibou57) wrote:
> Le Tue, 22 Nov 2011 16:02:06 +0100, Georg Bauhaus <rm.dash-bauhaus@futureapps.de> a écrit:
>> [1] http://www.eiffel.com/developers/design_by_contract_in_detail.html
> Oops, not good for its claims, an exemple DbC™ use case in this page is erroneous:

Care to show where the error is?

>> it will look as follows in Eiffel syntax, as part of a genericclass DICTIONARY [ELEMENT]:
>>
>> put (x: ELEMENT; key: STRING) is
>> -- Insert x so that it will be retrievable through key.
>> require
>>   count <= capacity
>>   not key.empty
>> do
>> ... Some insertion algorithm ...
>> ensure
>>   has (x)
>>   item (key) = x  count = old count + 1
>> end
> The post-condition may fails, while the pre-condition was fulfilled (unless class DICTIONARY is weird). At least, a good candidate for a legitimate exception raise :p

`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?

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

[Dmitry A. Kazakov]

On Wed, 23 Nov 2011 00:52:23 +0100, Georg Bauhaus wrote:

> On 22.11.11 20:15, Dmitry A. Kazakov wrote:
> 
>>> Meyer: "Programming is a human activity".
>>> Programmers are led towards a solution during the process of programming.
>>> Depending on the characteristics of the process, then,
>>> programmers will produce different results.
>>
>> I see no word "debugging" there.
> 
> A debugging aid is a means of finding mistakes when developing programs.

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.

>>> DbC (TM), as a characteristic of a process, leads to products
>>> that lend themselves to proving them correct more than others,
>>> provided this is possible.
>>
>> I suppose drinking coffee does that as well.
> 
> No, coffee is not known to yield better manifestations of intended
> subprogram behavior in source text, certainly not better than specifying
> conditions (program states) framing possible executions.

Really? I bet that coffee is far more helpful than frantic patching the
program in the debugger.

>> Note that all
>> the buzz is about noticing something unanticipated.
> 
> If a description of possible program states in not exhaustive,
> then, nevertheless, this description establishes a non-empty set
> of states, and another non-empty set, its complement.

It is a useless description because it is not constructive (undecidable).
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.

>> I see the point, since it is impossible do right, you are going to do it
>> wrong. I am not arguing for or against your or Meyer's motivations. I only
>> state that it is wrong.
> 
> You do use compilers, and since it is impossible to know their behavior in
> general, are you doing wrong?

Yep, you see an executable attachment to an e-mail. Trust me, it is wrong
to open it!

> There is no right or wrong in most programs.

You cannot build safe software on false premises. You could bring thousands
reasons, but none can change the fact. What is wrong is wrong. 

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Simon Wright]

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

> It is lousy language design placing implementation (executable code
> ensuring the desired behavior, e.g. raising exception) into
> declarations.

Are you just talking about [post]conditions? because it's not uncommon
to use complex declarative regions for run-time array bounds etc, which
will include the possibility of exceptions.

[Does SPARK forbid such declarative constructs?]

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

[Yannick Duchêne (Hibou57)]

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.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: [Epigrams on Programming — Alan J. — P. Yale University]

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

[Georg Bauhaus]

On 23.11.11 09:44, Dmitry A. Kazakov wrote:

> It is lousy language design placing implementation (...) into declarations.

As said, the goal is to make postcondition a consequence
of the program without postcondition, and redundant.

   type T is new Ada.Finalization.Controlled with ...;

   overriding procedure Adjust (Object : in out T);

   procedure Op (Item : in out T);

Is there no executable code?


> The proper one is:
>
>     procedure ...
>        raise Contraint_Error; -- I don't tell you when and how


So I won't know what my client code has done wrong.
How am I to learn how to do it right?  Trial and error?

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

[Dmitry A. Kazakov]

On Wed, 23 Nov 2011 09:32:20 +0000, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> It is lousy language design placing implementation (executable code
>> ensuring the desired behavior, e.g. raising exception) into
>> declarations.
> 
> Are you just talking about [post]conditions? because it's not uncommon
> to use complex declarative regions for run-time array bounds etc, which
> will include the possibility of exceptions.

Such constructs are certainly not welcome. However declaration of a local
variable requiring some elaboration that may fail is one thing, placing
executable semantically loaded code into the interfaces is extreme.
Implementation belongs to the bodies.

If you mean dynamic constraints, yes it is very dangerous stuff, which must
be handled by the language with a great care. I think Ada 83-95 found a
balance here.

P.S. I hope everybody agrees that dynamic pre-/post-conditions are a part
of the implementation? The rest is simple. [A comparable case is barriers
of entries.]

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Dmitry A. Kazakov]

On Wed, 23 Nov 2011 10:54:18 +0100, Georg Bauhaus wrote:

> On 23.11.11 09:44, Dmitry A. Kazakov wrote:
> 
>> The proper one is:
>>
>>     procedure ...
>>        raise Contraint_Error; -- I don't tell you when and how
> 
> So I won't know what my client code has done wrong.

The client code cannot do anything illegal. Constraint_Error is a valid
behavior.

[In terms of preconditions, in a properly designed program all dynamic
preconditions are trivially true.]

> How am I to learn how to do it right?

To do what? Program semantics is your business. How do you learn to call
sine instead of sqrt?

> Trial and error?

Understanding the problem domain, consulting the customer, reading design
manual, drinking coffee with sugar...

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Brian Drummond]

On Wed, 23 Nov 2011 09:32:20 +0000, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> It is lousy language design placing implementation (executable code
>> ensuring the desired behavior, e.g. raising exception) into
>> declarations.
> 
> ...it's not uncommon
> to use complex declarative regions for run-time array bounds etc, which
> will include the possibility of exceptions.
> 
> [Does SPARK forbid such declarative constructs?]

[as I am about 3/4 of the way through reading Barnes : High Integrity 
Software : yes it does. Storage allocation is completely determinable at 
elaboration time, so you can prove everything will fit, long before you 
turn the ignition key]

[ - Brian]

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

[Georg Bauhaus]

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.

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

[Georg Bauhaus]

On 23.11.11 10:56, Dmitry A. Kazakov wrote:

> P.S. I hope everybody agrees that dynamic pre-/post-conditions are a part
> of the implementation?

I don't agree. pre/post should specify what the implementation is
supposed to do.

CS trivia that programs behave differently depending on
Assertion_Policy simply do not matter, since the goal is
to arrive at programs whose checks are a consequence of the
program without them: turn assertion checking off and the
program's effect on the environment are the same. "The same"
means: for all relevant precisions of measurement of "same effect".

> The rest is simple. [A comparable case is barriers
> of entries.]

No!  Absolutely incomparable intent!

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

[Dmitry A. Kazakov]

On Wed, 23 Nov 2011 12:03:34 +0100, Georg Bauhaus wrote:

> On 23.11.11 10:56, Dmitry A. Kazakov wrote:
> 
>> P.S. I hope everybody agrees that dynamic pre-/post-conditions are a part
>> of the implementation?
> 
> I don't agree. pre/post should specify what the implementation is
> supposed to do.

In that case they cannot be executable.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Georg Bauhaus]

On 23.11.11 10:04, Dmitry A. Kazakov wrote:
> On Wed, 23 Nov 2011 00:52:23 +0100, Georg Bauhaus wrote:
>
>> On 22.11.11 20:15, Dmitry A. Kazakov wrote:
>>
>>>> Meyer: "Programming is a human activity".
>>>> Programmers are led towards a solution during the process of programming.
>>>> Depending on the characteristics of the process, then,
>>>> programmers will produce different results.
>>>
>>> I see no word "debugging" there.
>>
>> A debugging aid is a means of finding mistakes when developing programs.
>
> 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.

Since designing with annotations (instead of without them, or with
comments only)  happens at the level of abstract data types,
DbC absolutely wants programmers to be honest about the
bugs in their ADTs' interfaces.  These bugs exist
in brains, on paper, or in package specs. Or, well, as aspects.
At this stage, one cannot use a debugger for executable programs,
because there is no program.  But there are bugs already.
DbC need not happen at the level of concrete implementation (again,
being finally a non-trivial, but redundant consequence of the
annotated program). In fact, DbC emphasizes that assertions
do not replace conditionals.


> I bet that coffee is far more helpful than frantic patching the
> program in the debugger.

What debugger?


> 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?
ADTs without invariants?
Subprograms of unknown effect, but possibly raising a ubiquitous exception?
Yes, it is possible to understand these things, but I don't understand
how this is so useful in comparison.


>> 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,
they are not safe, but they are pretty safe. Yes, pretty safe.
That's bad, but it is something. Reduces risk of stress-induced
health problems caused by buggy programs.
My point is that it is better to reduce the number of annoyances
created by such programs, rather than to insist that ensuring
total safety is impossible in general.

> You could bring thousands
> reasons, but none can change the fact. What is wrong is wrong.

Wrong means wrong with respect to some formalism; the one given
is too trivial for my taste, or maybe I don't understand it.
I need proof of "wrong to do this", and will, like you, continue
to use compilers, which might be wrong.

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

[Georg Bauhaus]

On 23.11.11 12:13, Dmitry A. Kazakov wrote:
> On Wed, 23 Nov 2011 12:03:34 +0100, Georg Bauhaus wrote:
>
>> On 23.11.11 10:56, Dmitry A. Kazakov wrote:
>>
>>> P.S. I hope everybody agrees that dynamic pre-/post-conditions are a part
>>> of the implementation?
>>
>> I don't agree. pre/post should specify what the implementation is
>> supposed to do.
>
> In that case they cannot be executable.

 From the point of view of CS trivia, they cannot be executable.
But this point of view is not applicable, which---for me---is
the good bit about Assertion_Policy:
The goal is to have program P = program P' where the difference
between P and P' is different Assertion_Policy.  Again, CS trivia
about the general theoretical impossibility of = are too trivial
to be helpful.

Note that DbC emphasizes that assertions do not replace if-statements.

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

[Dmitry A. Kazakov]

On Wed, 23 Nov 2011 12:25:56 +0100, Georg Bauhaus wrote:

> On 23.11.11 12:13, Dmitry A. Kazakov wrote:
>> On Wed, 23 Nov 2011 12:03:34 +0100, Georg Bauhaus wrote:
>>
>>> On 23.11.11 10:56, Dmitry A. Kazakov wrote:
>>>
>>>> P.S. I hope everybody agrees that dynamic pre-/post-conditions are a part
>>>> of the implementation?
>>>
>>> I don't agree. pre/post should specify what the implementation is
>>> supposed to do.
>>
>> In that case they cannot be executable.
> 
>  From the point of view of CS trivia, they cannot be executable.
> But this point of view is not applicable,

I don't see why doing something wrong should make it more applicable. Maybe
because the criteria of applicability are distorted as well?

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Dmitry A. Kazakov]

On Wed, 23 Nov 2011 12:15:30 +0100, Georg Bauhaus wrote:

> On 23.11.11 10:04, Dmitry A. Kazakov wrote:
>> On Wed, 23 Nov 2011 00:52:23 +0100, Georg Bauhaus wrote:
>>
>>> On 22.11.11 20:15, Dmitry A. Kazakov wrote:
>>>
>>>>> Meyer: "Programming is a human activity".
>>>>> Programmers are led towards a solution during the process of programming.
>>>>> Depending on the characteristics of the process, then,
>>>>> programmers will produce different results.
>>>>
>>>> I see no word "debugging" there.
>>>
>>> A debugging aid is a means of finding mistakes when developing programs.
>>
>> 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?

>> I bet that coffee is far more helpful than frantic patching the
>> program in the debugger.
> 
> What debugger?

A tool for debugging.

>> 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 which has nothing to do with the
specification. Different implementation will have different invariants,
evidently.

> Subprograms of unknown effect,

You confuse interface and implementation.

>>> 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.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Georg Bauhaus]

On 23.11.11 14:14, Dmitry A. Kazakov wrote:
> On Wed, 23 Nov 2011 12:25:56 +0100, Georg Bauhaus wrote:
> 
>> On 23.11.11 12:13, Dmitry A. Kazakov wrote:
>>> On Wed, 23 Nov 2011 12:03:34 +0100, Georg Bauhaus wrote:
>>>
>>>> On 23.11.11 10:56, Dmitry A. Kazakov wrote:
>>>>
>>>>> P.S. I hope everybody agrees that dynamic pre-/post-conditions are a part
>>>>> of the implementation?
>>>>
>>>> I don't agree. pre/post should specify what the implementation is
>>>> supposed to do.
>>>
>>> In that case they cannot be executable.
>>
>>  From the point of view of CS trivia, they cannot be executable.
>> But this point of view is not applicable,
> 
> I don't see why doing something wrong should make it more applicable. Maybe
> because the criteria of applicability are distorted as well?

If it is wrong to assume that a compiler is correct
(which is why there is verification of object code),
then, since we use compilers regardless, there exists
a criterion that applies when we use compilers.
Formal CS is thus overridden.

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

[Georg Bauhaus]

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!".

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

[Dmitry A. Kazakov]

On Wed, 23 Nov 2011 14:59:31 +0100, Georg Bauhaus wrote:

> On 23.11.11 14:14, Dmitry A. Kazakov wrote:
>> On Wed, 23 Nov 2011 12:25:56 +0100, Georg Bauhaus wrote:
>> 
>>> On 23.11.11 12:13, Dmitry A. Kazakov wrote:
>>>> On Wed, 23 Nov 2011 12:03:34 +0100, Georg Bauhaus wrote:
>>>>
>>>>> On 23.11.11 10:56, Dmitry A. Kazakov wrote:
>>>>>
>>>>>> P.S. I hope everybody agrees that dynamic pre-/post-conditions are a part
>>>>>> of the implementation?
>>>>>
>>>>> I don't agree. pre/post should specify what the implementation is
>>>>> supposed to do.
>>>>
>>>> In that case they cannot be executable.
>>>
>>>  From the point of view of CS trivia, they cannot be executable.
>>> But this point of view is not applicable,
>> 
>> I don't see why doing something wrong should make it more applicable. Maybe
>> because the criteria of applicability are distorted as well?
> 
> If it is wrong to assume that a compiler is correct

It is right that the compiler correctly translates your program. Are you
suggesting to break the compiler because it might be already broken?

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Robert A Duff]

"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> writes:

> Le Mon, 21 Nov 2011 14:08:04 +0100, Robert A Duff
> <bobduff@shell01.theworld.com> a �crit:
>> 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.

> Please, an example! :)

In 4.6:

39.1/2    * {AI95-00392-01} If the component types of the array types are
            anonymous access types, then a check is made that the
            accessibility level of the operand type is not deeper than that of
            the target type.

[Program_Error is raised at run time if this check fails.]

39.b/2      Reason: This check is needed for operands that are access
            parameters and in instance bodies. Other cases are handled by the
            legality rule given previously.

If there are no access parameters involved, most implementations will
check this rule at compile time of the instance, and give a warning.
The only reason it needs to be a run-time check is to avoid breaking
the contract model (ignoring the access parameter case), which is
sort of a "cheat".

- Bob

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

[Simon Wright]

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

> P.S. I hope everybody agrees that dynamic pre-/post-conditions are a
> part of the implementation?

I think I don't actually care that much!

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

[Georg Bauhaus]

On 23.11.11 15:43, Dmitry A. Kazakov wrote:
> On Wed, 23 Nov 2011 14:59:31 +0100, Georg Bauhaus wrote:
> 
>> On 23.11.11 14:14, Dmitry A. Kazakov wrote:
>>> On Wed, 23 Nov 2011 12:25:56 +0100, Georg Bauhaus wrote:
>>>
>>>> On 23.11.11 12:13, Dmitry A. Kazakov wrote:
>>>>> On Wed, 23 Nov 2011 12:03:34 +0100, Georg Bauhaus wrote:
>>>>>
>>>>>> On 23.11.11 10:56, Dmitry A. Kazakov wrote:
>>>>>>
>>>>>>> P.S. I hope everybody agrees that dynamic pre-/post-conditions are a part
>>>>>>> of the implementation?
>>>>>>
>>>>>> I don't agree. pre/post should specify what the implementation is
>>>>>> supposed to do.
>>>>>
>>>>> In that case they cannot be executable.
>>>>
>>>>  From the point of view of CS trivia, they cannot be executable.
>>>> But this point of view is not applicable,
>>>
>>> I don't see why doing something wrong should make it more applicable. Maybe
>>> because the criteria of applicability are distorted as well?

Because it leads to self documenting source text that
uses this wrong formalism, assertions.


>> If it is wrong to assume that a compiler is correct
> 
> It is right that the compiler correctly translates your program.

We do not know whether or not a compiler correctly translates
a given program unless we show that the translation
is correct. If we do, we know that the given run of the compiler
on the given program seems to have worked as intended. (ACATS)
The only check in a compiler without internal checks is a translation
that is checked by humans.  A compiler that performs internal checks
while it is running may fail and produce a notice of failure.
Perhaps it should continue instead and produce a program that
shifts a rocket?

Is there a compiler out there that is know to work correctly for
a set of programs?  In this compiler, DbC assertions will
be documentation only.

> Are you
> suggesting to break the compiler because it might be already broken?

No.

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

[Dmitry A. Kazakov]

On Wed, 23 Nov 2011 15:42:25 +0100, Georg Bauhaus wrote:

> 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

Tell whom and what? That reminds me the notorious "message not understood."
It is contradicts to basic principles of engineering, but I don't want to
go into it.

>>> ADTs without invariants?
>> 
>> Invariant is an implementation detail
> 
> No, there is no implementation in a DbC contract.

Great!

>>> 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?

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.

>>>>> 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.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Dmitry A. Kazakov]

On Wed, 23 Nov 2011 17:10:41 +0100, Georg Bauhaus wrote:

> On 23.11.11 15:43, Dmitry A. Kazakov wrote:
>> On Wed, 23 Nov 2011 14:59:31 +0100, Georg Bauhaus wrote:
>> 
>>> If it is wrong to assume that a compiler is correct
>> 
>> It is right that the compiler correctly translates your program.
> 
> We do not know whether or not a compiler correctly translates
> a given program unless we show that the translation
> is correct.

It is no matter if we know it or not. The program legality is independent
on that knowledge.

> Is there a compiler out there that is know to work correctly for
> a set of programs?  In this compiler, DbC assertions will
> be documentation only.

Huh, are you going to detect compiler bugs using preconditions? That is the
silliest thing, next to run-time contract checks:

   X := 1;
   if X = 1 then
     -- Wait, that is not enough the compiler might got "=" broken!
     if X/=2 and X/=3 and X/=4 ... X/=Positive'Last then
        -- That must give X=1, but, what if and is broken?
        if not (X=2 or X=3 or X=4 ...
           -- and so on until we notice that X might be actually Y, "if" be
           -- "while" etc

I don't believe Meyer would claim that. Did he?

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Dmitry A. Kazakov]

On Wed, 23 Nov 2011 15:12:07 +0000, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> P.S. I hope everybody agrees that dynamic pre-/post-conditions are a
>> part of the implementation?
> 
> I think I don't actually care that much!

Should it mean that you don't care about separation of implementation and
interface?

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Georg Bauhaus]

On 23.11.11 20:51, Dmitry A. Kazakov wrote:
>
> are you going to detect compiler bugs using preconditions?

Some compilers have detected compiler bugs by using assertions
at runtime.

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

[Georg Bauhaus]

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.

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

[Shark8]

On Nov 22, 10:23 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Tue, 22 Nov 2011 16:02:06 +0100, Georg Bauhaus wrote:
> >>> I think that, with the exception of compiler-determines-all-of-this,
> >>> the above is a well known characterization of DbC.
>
> >> Not really. DbC is about upfront formalized requirements.
>
> > Not sure, are you speaking about DbC (TM)?
>
> I don't care about trade marks and definitions given by reference
> manuals...


Why not; definitions are essential to understanding each other.
If someone saying 'hammer' means 'shotgun' then what does "I need a
hammer." mean?

Now you could argue that the definition is irrelevant in an Ada forum
because it's from Eiffel's documentation; but a uniform rejection of
all RM definitions is just stupid.

>
> > (b) A debugging ("design", "specification", bla-bla) aid leading
> >     towards formally proven components where such proofs are possible.
>
> I cannot decipher this, sorry.

What it's saying is: "Design By Contract can aid in debugging and in
formally proving components for which it is possible to formally
prove."

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

[Shark8]

On Nov 22, 9:13 pm, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> A guess attempt: does not depend on Generic_Delete implementation, but
> rather on a Generic_Delete instantiation parameters. If you could post the
> instantiation snippet too… (with declarations it depends on).
>
> Le Sat, 19 Nov 2011 22:14:44 +0100, Shark8 <onewingedsh...@gmail.com> a
> écrit:
>
>
>
>
>
>
>
>
>
> > I was working on some simple little array manipulation functions when
> > I encountered an interesting behavior in the compiler; it said that
> > trying to instantiate a function of the form:
> >    Generic
> >       Type Element is Private;
> >       Type Index_Type is (<>);
> >       Type Array_Type is Array (Index_Type Range <>) of Element;
> >    Function Generic_Delete( Index : In Index_Type; Data : In
> > Array_Type ) Return Array_Type;
>
> > When given the following body, the compiler complained about the
> > Index_Range'First/Last not being static:
>
> >    Function Generic_Delete( Index : In Index_Type; Data : In
> > Array_Type ) Return Array_Type is
> >    begin
> >       if Index not in Data'Range then
> >          Raise Constraint_Error;
> >       else
> >            case Index is
> >            when Index_Type'First => Return
> > Data( Index_Type'Succ(Index)..Data'Last );
> >            when Index_Type'Last => Return
> > Data( Data'First..Index_Type'Pred(Index) );
> >            when others =>
> >                   Return Data( Data'First..Index_Type'Pred(Index) )
> >             & Data( Index_Type'Succ(Index)..Data'Last );
> >            end case;
> >       end if;
> >    end Generic_Delete;
>
> > Now, I know that the following works as a fix:
>
> >      Function Generic_Delete( Index : In Index_Type; Data : In
> > Array_Type ) Return Array_Type is
> >      begin
> >         if Index not in Data'Range then
> >            Raise Constraint_Error;
> >         else
> >            if Index = Data'First then
> >               Return Data( Index_Type'Succ(Index)..Data'Last );
> >            elsif Index = Data'Last then
> >               Return Data( Data'First..Index_Type'Pred(Index) );
> >            else
> >               Return Data( Data'First..Index_Type'Pred(Index) )
> >             & Data( Index_Type'Succ(Index)..Data'Last );
> >            end if;
> >         end if;
> >      end Generic_Delete;
>
> > But the question that came to my mind after reading the ARM section on
> > the error (sorry, I forgot to write it down) is, why is it not static?
> > Is it because though the elaboration-parameters *may* be known [and
> > static] at compile-time that some instantiation might NOT be
> > [guaranteed] to be known at compile-time? (i.e. because the compiler
> > cannot guarantee that you won't throw 1..N where N is something pulled
> > from the user-input?)
>
> --
> “Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on
> Programming — Alan J. — P. Yale University]
> “Structured Programming supports the law of the excluded muddle.” [Idem]

The type I was using were something like:
SubType Board_Index is Positive Range 1..9;
Type Column is Array( Board_Index Range <> ) of Board_Index;


So the instantiation was something like:
 Function Delete is New Generic_Delete( Board_Index, Board_Index,
Column );

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

[Yannick Duchêne (Hibou57)]

Le Thu, 24 Nov 2011 04:07:55 +0100, Shark8 <onewingedshark@gmail.com> a  
écrit:
> What it's saying is: "Design By Contract can aid in debugging and in
> formally proving components for which it is possible to formally
> prove."
Or alternatively, far too much long/difficult to prove. This may be  
compared to “this procedure must terminate in a reasonable amount of  
time”. That's indeed the difference between hard pure formalism and  
concrete things, and sooner or later, we need things to become concrete :)

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: [Epigrams on Programming — Alan J. — P. Yale University]

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

[stefan-lucks]

On Wed, 23 Nov 2011, Dmitry A. Kazakov wrote:

> That is exactly why contracts cannot be dynamic. Dynamic means statically
> undecidable. 

That point seems to be the main issue that makes this discussion going on 
and on ...

Dynamic means it has not been statically decided by an apprpriate tool 
(such as SPARK). 

Good contracts are statically decidable! I guess, few c.l.a. people will 
disagree and claim that good contracts are statically undecidable.

Now, if we have the tools to statically verify these contracts, then we 
are done. There is SPARK, but that very severely constrains Ada to be able 
to find proofs. Perhaps, within some time, there will be tools to 
statically verify some Ada 2012 contracts (google for HiLite Ada). 

In the meantime, Ada 2012 contracts are just claims made by the programmer 
(perhaps formally verified by hand or so). At this stage, what can you do?

  a) Documentation only -- the existence of the contract has no influence 
     on the compiled code. 
  
  b) Support for testing -- check the conditions during testing time, but 
     turn to (a) after testing has been done. (*)

  c) Organized panic -- write the event into a log file; if neccessary, 
     try to minimize the damage (e.g., write important data that has 
     recently been changed into a temporary file); shut down.

Ada 2012 supports all thee strategies (by using compiler switches), 
depending on the programmers' (or project mangagers') views and 
requirements. What should be wrong with this choice?

And sure, Ada 2012 seems to allow you to write really lousy contracts, 
less than useful, with side-effects and whatever. To some degree, with pre 
=> ..., post => ... is a bit like UNCHECKED_Something: useful when used 
with care, but dangerous.

---------
(*) This is what someone denoted as "debugging" support. I think, testing 
is the better notion here. 

-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

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

[Simon Wright]

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

> On Wed, 23 Nov 2011 15:12:07 +0000, Simon Wright wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>> 
>>> P.S. I hope everybody agrees that dynamic pre-/post-conditions are a
>>> part of the implementation?
>> 
>> I think I don't actually care that much!
>
> Should it mean that you don't care about separation of implementation
> and interface?

What I think I was trying to say was that it doesn't seem to me to make
a lot of difference whether the pre/post-conditions are
dynamic. Providing, of course, I've understood your point.

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.

I seem to be tempted into speculations about SPARK at this point. Stacks
seem to be a rather dangerous construct from the point of view of
proving correctness, logic not being very good at counting.

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

[Dmitry A. Kazakov]

On Thu, 24 Nov 2011 01:59:49 +0100, Georg Bauhaus wrote:

> On 23.11.11 20:51, Dmitry A. Kazakov wrote:
>>
>> are you going to detect compiler bugs using preconditions?
> 
> Some compilers have detected compiler bugs by using assertions
> at runtime.

I meant in an *application* program.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Dmitry A. Kazakov]

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 then that expression
is static, per definition of the word "expressed." When it cannot be
expressed then it is not.

A dynamic precondition does not express anything, because it is unknown
until run-time. If it is known, then it is not dynamic.

> I seem to be tempted into speculations about SPARK at this point. Stacks
> seem to be a rather dangerous construct from the point of view of
> proving correctness, logic not being very good at counting.

SPARK does it right, Eiffel and now Ada do it wrong.

My plea is not to full ourselves. If correctness cannot be proved
statically, then the requirement expressed by the precondition must be
considered as not satisfied. That precondition must be replaced by "true",
and the corresponding exception (Stack_Full) added to the postcondition.
The clients must respect this new contract and handle Stack_Full.

I would like Ada integrated rather with SPARK than with Eiffel, allowing
the programmer to choose between static correctness and, when that does not
work or seem to be too expensive, contracts extended with exceptions.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Dmitry A. Kazakov]

On Wed, 23 Nov 2011 19:07:55 -0800 (PST), Shark8 wrote:

> On Nov 22, 10:23�am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:

>> I don't care about trade marks and definitions given by reference
>> manuals...
> 
> Why not; definitions are essential to understanding each other.
> If someone saying 'hammer' means 'shotgun' then what does "I need a
> hammer." mean?

That is the reason. TM and RM are inclined to name hammer shotgun.

DbC (TM) considerably deviates from design by contract (common sense), as
Georg has explained willingly or not. For example disregarding separation
of interface and implementation is not how things are designed by contract.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Georg Bauhaus]

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.

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

[Dmitry A. Kazakov]

On Thu, 24 Nov 2011 02:36:47 +0100, Georg Bauhaus wrote:

> 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.

What is dynamic there?

> Similarly, for Sqrt, Ada throws Argument_Error if the caller
> fails to establish the implicit precondition of Sqrt:

It is not a precondition, sqrt (-1.0) is *defined* as Argument_Error
propagation. I.e. the postcondition includes Argument_Error. The
precondition is "X in Float."

> Is Sqrt'Result statically determinable?

The semantics of sqrt can be formally defined as it happens in math. For an
arithmetic based on bounded rational numbers with rounding errors (e.g.
Float) it is also possible, but nobody would care.

>>>>>>> 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.

It says that correctness is unconditional to our ability to decide it. [It
is conditional to the specifications only] 

A plane without fuel would crash regardless your ability to determine the
level kerosene in its tanks.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Georg Bauhaus]

On 24.11.11 11:10, Dmitry A. Kazakov wrote:

> DbC (TM) considerably deviates from design by contract (common sense), as
> Georg has explained willingly or not. For example disregarding separation
> of interface and implementation is not how things are designed by contract.

The client part of the contract as per DbC (TM) must be read without
referring to implementation. Contractual obligations follow from the
specs only. They consist of preconditions, postconditions, and
type invariant.

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

[Brian Drummond]

On Thu, 24 Nov 2011 08:07:45 +0000, Simon Wright wrote:

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

>>
>> Should it mean that you don't care about separation of implementation
>> and interface?
> 
> What I think I was trying to say was that it doesn't seem to me to make
> a lot of difference whether the pre/post-conditions are dynamic.
> Providing, of course, I've understood your point.

I think it does.

> 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.
> 
> I seem to be tempted into speculations about SPARK at this point. Stacks
> seem to be a rather dangerous construct from the point of view of
> proving correctness, logic not being very good at counting.

Indeed. But if you also prohibit recursion, maximum stack use is provable.

Spark is interesting in that some implementation facts (but not really 
details) do leak into the annotations (contracts) in the specification, 
though not into the Ada code for the specification. 

It has strategies to hide the details (this procedure modifies the state 
in that package, via an accessor) which are "refined" internally in the 
package implementation (the accessor modifies stack contents, stack 
pointer). 

But the state of the art seems to be that for contracts to be statically 
determinable, you must restrict how you program, compared to full Ada.

In this world, I come down on the side of: dynamically determinable 
contracts may not be perfect, but they are a lot better than nothing. I 
would use them and try to create tests to catch them out.

Ada is full of such implicit contracts, though they may have other names; 
some statically determinable...
for i in my_array'range loop 	-- I is contracted to be in range
and some dynamically determinable
a * 1000000	-- raises Constraint_Error if violated
and I don't see any objections to these (maybe from C programmers!)
so I think only good can come of the ability to create additional 
contracts.

Unless perhaps the programmer gains a false sense of security from having 
written contracts. But how is that any different from using the implicit 
ones?

Perhaps the best that can be hoped for is an assessment of each contract 
by the compiler (or proof tool), and a "WARNING: may raise exception" for 
the not-proven, to minimise such complacency.

- Brian

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

[Georg Bauhaus]

On 24.11.11 11:52, Dmitry A. Kazakov wrote:

>> 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.
>
> What is dynamic there?

Its initial capacity, as outlined in another post.
One may continue with current_number_of_items and such.

> It is not a precondition, sqrt (-1.0) is *defined* as Argument_Error
> propagation. I.e. the postcondition includes Argument_Error. The
> precondition is "X in Float."

As a precondition for { Sqrt'Result in Float_Type'Base } the LRM states
{ X in Float_Type'Base and X >= 0.0 }. The precondition of Sqrt in
some language that defines Argument_Error in Float_Type'Base is different.
Not wrong, possibly desirable, but different.


> A plane without fuel would crash regardless your ability to determine the
> level kerosene in its tanks.

Yes, but we do not know before fly-time whether or not there
is going to be enough fuel in the tanks. Flying loops consuming more,
hardware errors caused by people shooting at wings, etc., will not
stop the plane designers to state, using arithmetic expressions,
how much fuel it takes (precondition) to fly from A to B.

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

[Dmitry A. Kazakov]

On Thu, 24 Nov 2011 12:30:46 +0100, Georg Bauhaus wrote:

> On 24.11.11 11:52, Dmitry A. Kazakov wrote:
> 
>>> 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.
>>
>> What is dynamic there?
> 
> Its initial capacity, as outlined in another post.

You wrote about certain capacity, that is static.

> One may continue with current_number_of_items and such.

Same here, the contract that Push does not raise if n < N is static.
Otherwise the reader of the contract could not understand it. Whatever
predicate about a type as whole you must be either true or false for all
instances of that type.

>> It is not a precondition, sqrt (-1.0) is *defined* as Argument_Error
>> propagation. I.e. the postcondition includes Argument_Error. The
>> precondition is "X in Float."
> 
> As a precondition for { Sqrt'Result in Float_Type'Base } the LRM states
> { X in Float_Type'Base and X >= 0.0 }.

E.g. for sqrt=2.0, X in Float and X=4.0, etc.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Dmitry A. Kazakov]

On Thu, 24 Nov 2011 11:49:30 +0100, Georg Bauhaus wrote:

> On 24.11.11 10:27, Dmitry A. Kazakov wrote:

>> 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,

There is no such thing as assumption, there are only conditions for
whatever outcome of which, the program's behavior must be defined.

> Like when showing that for a stack object, the sequence
> (not Is_Full, Push, Pop) is a safe sequence,

It is not safe:

1. finalization and initialization may fail in Ada. The contracts of
element and index types propagate into the contracts of the container.

2. immutable stack has one Is_Full.

And it is the behavior, not the contract. The contract might imply behavior
(safety of this sequence under certain conditions), when provable. If not
provable, adding dynamic checks in all possible places trying Push and Pop
would be pointless. Not proven means: expect any outcome (any = anything
not excluded by a proof).

It is also pointless to use undecidable propositions for static proofs
(which is basically the idea behind dynamic checks). Garbage in, garbage
out.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Georg Bauhaus]

On 24.11.11 14:14, Dmitry A. Kazakov wrote:

> There is no such thing as assumption, there are only conditions for
> whatever outcome of which, the program's behavior must be defined.

When I state a condition and have no proof that the condition
is correct WRT such-and-such, then my statement is based on
assumptions. Let's be honest.

BTW, assuming looks like a normal mathematical gesture to me:
"Assuming that P(x, y) is true, we show that Q(x, y, z) is true."
Why do mathematicians do this if their work hinges on statically
unproven P(x, y)?

>> Like when showing that for a stack object, the sequence
>> (not Is_Full, Push, Pop) is a safe sequence,
> 
> It is not safe:

I didn't say that it is safe. I said it is (a) safe sequence, ceteris
paribus (listing these) and (b) safe sequence because, to quote you,
"The contract might imply behavior (safety of this sequence
under certain conditions), when provable."  The sequence of operations
  (not Is_Full, Push, Pop)
is provably o.K. by the contract shown because of a 1:1 correspondence
of the type's invariant (ensuring capacity and not Is_Full),
the postconditions and preconditions at each step. Therefore,
checks will be redundant.

> 2. immutable stack has one Is_Full.

If by immutable you mean a constant view, what's the point?
If by immutable you mean a discriminant won't change,
Is_Full may still not be constant function. I guess I don't understand.


> It is also pointless to use undecidable propositions for static proofs
> (which is basically the idea behind dynamic checks). Garbage in, garbage
> out.

Yes. If I knew SPARK better, I might say something about
proof functions, but I don't.

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

[Georg Bauhaus]

On 24.11.11 13:52, Dmitry A. Kazakov wrote:
> On Thu, 24 Nov 2011 12:30:46 +0100, Georg Bauhaus wrote:
> 
>> On 24.11.11 11:52, Dmitry A. Kazakov wrote:
>>
>>>> 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.
>>>
>>> What is dynamic there?
>>
>> Its initial capacity, as outlined in another post.
> 
> You wrote about certain capacity, that is static.

The certainty of an initial capacity is static, its value
isn't, so the check cannot, in general, be performed until
run-time. Perhaps in special cases whole program analysis
can move the check to compile time.
(Also, http://www.merriam-webster.com/dictionary/certain)


>> One may continue with current_number_of_items and such.
> 
> Same here, the contract that Push does not raise if n < N is static.

Ehr, yes, the contract guides programmers and the check may be
performed at run-time ...

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

[Dmitry A. Kazakov]

On Thu, 24 Nov 2011 15:31:27 +0100, Georg Bauhaus wrote:

> On 24.11.11 14:14, Dmitry A. Kazakov wrote:
> 
>> There is no such thing as assumption, there are only conditions for
>> whatever outcome of which, the program's behavior must be defined.
> 
> When I state a condition and have no proof that the condition
> is correct WRT such-and-such, then my statement is based on
> assumptions.

No, "if A then B" is not based on an assumption of A. B is (in this
context).

> BTW, assuming looks like a normal mathematical gesture to me:
> "Assuming that P(x, y) is true, we show that Q(x, y, z) is true."
> Why do mathematicians do this if their work hinges on statically
> unproven P(x, y)?

Because the mathematician usually stops at P|=Q. In programming you are
interested in both P|=... and ^P|=..., so long P is not proven.

>>> Like when showing that for a stack object, the sequence
>>> (not Is_Full, Push, Pop) is a safe sequence,
>> 
>> It is not safe:
> 
> I didn't say that it is safe. I said it is (a) safe sequence, ceteris
> paribus (listing these) and (b) safe sequence because, to quote you,
> "The contract might imply behavior (safety of this sequence
> under certain conditions), when provable."  The sequence of operations
>   (not Is_Full, Push, Pop)
> is provably o.K. by the contract shown because of a 1:1 correspondence
> of the type's invariant (ensuring capacity and not Is_Full),
> the postconditions and preconditions at each step. Therefore,
> checks will be redundant.

OK
 
>> 2. immutable stack has one Is_Full.
> 
> If by immutable you mean a constant view, what's the point?

That the proposition does not hold for all instances of stack.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Simon Wright]

Brian Drummond <brian@shapes.demon.co.uk> writes:

> Indeed. But if you also prohibit recursion, maximum stack use is
> provable.

Maximum use of a bounded buffer faced with a peaky input is probably
less provable. At least you have more potential solutions there; throw
away the earliest, throw away the latest, throw away the least
important.

> But the state of the art seems to be that for contracts to be
> statically determinable, you must restrict how you program, compared
> to full Ada.

And maybe the sort of system you try to prove?

The provably-correct part of a system will probably not be the whole of
it, not of course that that releases us from the obligation to prove as
much as possible. Even Tokeneer would have needed mitigations against
villains with chainsaws.

> In this world, I come down on the side of: dynamically determinable
> contracts may not be perfect, but they are a lot better than
> nothing. I would use them and try to create tests to catch them out.

A real-world approach!

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

[Shark8]

On Nov 24, 4:10 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Wed, 23 Nov 2011 19:07:55 -0800 (PST), Shark8 wrote:
> > On Nov 22, 10:23 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> > wrote:
> >> I don't care about trade marks and definitions given by reference
> >> manuals...
>
> > Why not; definitions are essential to understanding each other.
> > If someone saying 'hammer' means 'shotgun' then what does "I need a
> > hammer." mean?
>
> That is the reason. TM and RM are inclined to name hammer shotgun.
>
> DbC (TM) considerably deviates from design by contract (common sense),

Unfortunately "common sense" is not intuitively obvious to everyone;
furthermore, "common sense" is hampered by the fact that natural-
language tends to contain connotations not within the actual
definitions of the words. It is because of this that there must be a
set of definitions wherewich to have a common ground. (i.e. relying on
'common sense' you tend to argue about the definition-content rather
than the problem itself.)


> as
> Georg has explained willingly or not. For example disregarding separation
> of interface and implementation is not how things are designed by contract.

I actually fail to see exactly where the interface/implementation
separation is an issue in Ada 2012.
Consider this:
The ARM allows a compiler to treat PROCEDURE P( EXTERNAL_PARAM : IN
OUT SOME_TYPE ) IS [SUBPROGRAM_TEXT] END P; as the following:

PROCEDURE P( EXTERNAL_PARAM : IN OUT SOME_TYPE ) IS
INTERNAL_PARAM : SOME_TYPE:= EXTERNAL_PARAM;
[SUBPROGRAM_TEXT] (renaming EXTERNAL_PARAM to INTERNAL_PARAM)
EXTERNAL_PARAM := INTERNAL_PARAM;
END P;

Now, with the pre- and post-conditions we may expand this PROCEDURE
P( EXTERNAL_PARAM : IN OUT SOME_TYPE ) WITH PRE => PRECONDITION, POST
=> POSTCONDITION IS ... conceptually to:


PROCEDURE P( EXTERNAL_PARAM : IN OUT SOME_TYPE ) IS
IF NOT PRECONDITION RAISE CONSTRAINT_ERROR;
INTERNAL_PARAM : SOME_TYPE:= EXTERNAL_PARAM;
[SUBPROGRAM_TEXT] (renaming EXTERNAL_PARAM to INTERNAL_PARAM)
IF NOT POSTCONDITION RAISE CONSTRAINT_ERROR;
EXTERNAL_PARAM := INTERNAL_PARAM;
END P;

In other words, it seems to me to be the natural progression of Ada
2005's Null Exclusion.
Procedure Delete( Param : Not Null Access Link_List_Node ) is
 begin
   [Deletion operation] -- Hey, we can get rid of checking for Param =
Null here!
 end Delete;

By moving the null-exclusion logic "to the parameter" we can get rid
of all the cases where, previously, we had to handle Null. Likewise,
the pre- and post- conditions allow us to do the same on a more
generalized level. Just like, in simple terms, we can disregard
worrying about division-by-zero errors in the following code:

If Input_2 = 0 Then
 -- If Input_2 is Zero here we have a BIG PROBLEM.
 Return Input_1 / Input_2;  -- Return the division, if it is
possible...
Else
  Return Input_1'Base'Last; -- Otherwise, return the maximum value.
End If;

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

[Brian Drummond]

On Thu, 24 Nov 2011 18:12:30 +0000, Simon Wright wrote:

> Brian Drummond <brian@shapes.demon.co.uk> writes:
> 
>> Indeed. But if you also prohibit recursion, maximum stack use is
>> provable.
> 
> Maximum use of a bounded buffer faced with a peaky input is probably
> less provable. At least you have more potential solutions there; throw
> away the earliest, throw away the latest, throw away the least
> important.

Or,  input above a given peak rate is a violation of the preconditions.

>> But the state of the art seems to be that for contracts to be
>> statically determinable, you must restrict how you program, compared to
>> full Ada.
> 
> And maybe the sort of system you try to prove?

Or how much of the system you prove. There are ways to hide the rest from 
the examiner; Barnes has examples involving imported C functions...

> The provably-correct part of a system will probably not be the whole of
> it, not of course that that releases us from the obligation to prove as
> much as possible. Even Tokeneer would have needed mitigations against
> villains with chainsaws.

Yes. Other examples might be a GUI interface to a secure system. You 
would like to prove the input sanitization as well as the secure core, 
but everything outside that is probably a hopeless case...

- Brian

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

[Yannick Duchêne (Hibou57)]

Le Thu, 24 Nov 2011 23:48:46 +0100, Shark8 <onewingedshark@gmail.com> a  
écrit:
> Just like, in simple terms, we can disregard
> worrying about division-by-zero errors in the following code:
>
> If Input_2 = 0 Then
>  -- If Input_2 is Zero here we have a BIG PROBLEM.
>  Return Input_1 / Input_2;  -- Return the division, if it is
> possible...
> Else
>   Return Input_1'Base'Last; -- Otherwise, return the maximum value.
> End If;

You meant `If Input_2 /= 0 Then` ?

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: [Epigrams on Programming — Alan J. — P. Yale University]

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

[Dmitry A. Kazakov]

On Thu, 24 Nov 2011 14:48:46 -0800 (PST), Shark8 wrote:

> On Nov 24, 4:10�am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> On Wed, 23 Nov 2011 19:07:55 -0800 (PST), Shark8 wrote:
>>> On Nov 22, 10:23�am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
>>> wrote:
>>>> I don't care about trade marks and definitions given by reference
>>>> manuals...
>>
>>> Why not; definitions are essential to understanding each other.
>>> If someone saying 'hammer' means 'shotgun' then what does "I need a
>>> hammer." mean?
>>
>> That is the reason. TM and RM are inclined to name hammer shotgun.
>>
>> DbC (TM) considerably deviates from design by contract (common sense),
> 
> Unfortunately "common sense" is not intuitively obvious to everyone;
> furthermore, "common sense" is hampered by the fact that natural-
> language tends to contain connotations not within the actual
> definitions of the words.

It is still better than arbitrary slogans and advertising TMs and some RMs
tend to. If you want definitions, they should be from scientific sources,
peer reviewed, commonly accepted, [not funded by large vendors we all have
in mind...].

Then a definition must *define* some really existing phenomenon. It is
pointless to discuss DbC (TM) because it is not something which really
exists.

>> as
>> Georg has explained willingly or not. For example disregarding separation
>> of interface and implementation is not how things are designed by contract.
> 
> I actually fail to see exactly where the interface/implementation
> separation is an issue in Ada 2012.

Executable code in declarations is. Dynamic contracts are.

> In other words, it seems to me to be the natural progression of Ada
> 2005's Null Exclusion.
> Procedure Delete( Param : Not Null Access Link_List_Node ) is
>  begin
>    [Deletion operation] -- Hey, we can get rid of checking for Param =
> Null here!
>  end Delete;

Passing null is not a contract violation.

If the goal was to extend composition means in Ada, .e.g. an ability to
compose new operation F as

   F = Epilogue o G o Prologue 

I am not against that because I proposed such stuff myself. Just do not
call Prologue precondition, because it is not.

BTW, precondition, postcondition etc were introduced by Dijkstra for
correctness proofs. It is DbC (TM) which misuses established terms, not me.

> By moving the null-exclusion logic "to the parameter" we can get rid
> of all the cases where, previously, we had to handle Null.

Only when provable, i.e. when the compiler and the program reader *know*
that the check is superfluous in the body.

Note that there is much more use in statically enforced Prologue and
Epilogue. E.g. it would allow to solve the notorious problem of handling
dimensioned values in Ada. It is also necessary to have broken Ada
constructors and destructors working.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Dmitry A. Kazakov]

On Thu, 24 Nov 2011 15:45:10 +0100, Georg Bauhaus wrote:

> On 24.11.11 13:52, Dmitry A. Kazakov wrote:
>> On Thu, 24 Nov 2011 12:30:46 +0100, Georg Bauhaus wrote:
>> 
>>> On 24.11.11 11:52, Dmitry A. Kazakov wrote:
>>>
>>>>> 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.
>>>>
>>>> What is dynamic there?
>>>
>>> Its initial capacity, as outlined in another post.
>> 
>> You wrote about certain capacity, that is static.
> 
> The certainty of an initial capacity is static, its value
> isn't,

Therefore that value cannot be contracted upfront. You can only contract a
range of values, which is static.

>>> One may continue with current_number_of_items and such.
>> 
>> Same here, the contract that Push does not raise if n < N is static.
> 
> Ehr, yes, the contract guides programmers and the check may be
> performed at run-time ...

Unknown things cannot guide.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

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

[Georg Bauhaus]

On 11/25/11 10:47 AM, Dmitry A. Kazakov wrote:

> Then a definition must *define* some really existing phenomenon. It is
> pointless to discuss DbC (TM) because it is not something which really
> exists.

ISO/IEC 25436:2006
Also ECMA-367 section 8.9

If Ada's pre/post aspects are close to ECMA-367 section 8.9 and if
the latter is as flawed as the former, if so, then Ada can get it
right now: now is the time to fix bugs in Ada 2012. If there  is
a replacement such as
  F = Prologue o G o Epilogue
that is better than what is currently being added as pre/post aspects,
more correct, less buggy: now's the time.

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

[Yannick Duchêne (Hibou57)]

Le Fri, 25 Nov 2011 11:15:17 +0100, Georg Bauhaus  
<rm-host.bauhaus@maps.futureapps.de> a écrit:
> If Ada's pre/post aspects are close to ECMA-367 section 8.9 and if
> the latter is as flawed as the former, if so, then Ada can get it
> right now: now is the time to fix bugs in Ada 2012. If there  is
> a replacement such as
>   F = Prologue o G o Epilogue
> that is better than what is currently being added as pre/post aspects,
> more correct, less buggy: now's the time.
Clarification needed (cheese): you suggest to replace pre/post with  
function composition ? I'm not sure I've understood…


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: [Epigrams on Programming — Alan J. — P. Yale University]

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

[Georg Bauhaus]

On 25.11.11 10:47, Dmitry A. Kazakov wrote:

> BTW, precondition, postcondition etc were introduced by Dijkstra for
> correctness proofs. It is DbC (TM) which misuses established terms, not me.

 "I thought that testing would be an increasingly ineffective way
of removing  errors from [programs getting larger]. I did not realize
that the success of tests is that they test the programmer,
not the program. (...)
 "My basic mistake was to set up proof in opposition to testing,
where in fact  both of them are valuable and mutually supportive ways
of accumulating evidence of the correctness and serviceability
of programs."
    -- Tony Hoare,
http://cacm.acm.org/magazines/2009/10/42360-retrospective-an-axiomatic-basis-for-computer-programming/fulltext

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

[Yannick Duchêne (Hibou57)]

Le Fri, 25 Nov 2011 16:45:39 +0100, Georg Bauhaus  
<rm.dash-bauhaus@futureapps.de> a écrit:
> http://cacm.acm.org/magazines/2009/10/42360-retrospective-an-axiomatic-basis-for-computer-programming/fulltext
Worthy paper, thanks for the link.


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: [Epigrams on Programming — Alan J. — P. Yale University]

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

[Yannick Duchêne (Hibou57)]

Le Fri, 25 Nov 2011 16:45:39 +0100, Georg Bauhaus  
<rm.dash-bauhaus@futureapps.de> a écrit:
>  "I thought that testing would be an increasingly ineffective way
> of removing  errors from [programs getting larger]. I did not realize
> that the success of tests is that they test the programmer,
> not the program. (...)
>  "My basic mistake was to set up proof in opposition to testing,
> where in fact  both of them are valuable and mutually supportive ways
> of accumulating evidence of the correctness and serviceability
> of programs."
>     -- Tony Hoare,

I like this one too:
> Formal methods for achieving correctness must supportthe intuitive  
> judgment of programmers, not replace it.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: [Epigrams on Programming — Alan J. — P. Yale University]

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

[Shark8]

On Nov 25, 3:25 am, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Le Thu, 24 Nov 2011 23:48:46 +0100, Shark8 <onewingedsh...@gmail.com> a
> écrit:
>
> > Just like, in simple terms, we can disregard
> > worrying about division-by-zero errors in the following code:
>
> > If Input_2 = 0 Then
> >  -- If Input_2 is Zero here we have a BIG PROBLEM.
> >  Return Input_1 / Input_2;  -- Return the division, if it is
> > possible...
> > Else
> >   Return Input_1'Base'Last; -- Otherwise, return the maximum value.
> > End If;
>
> You meant `If Input_2 /= 0 Then` ?
>
> --
> “Syntactic sugar causes cancer of the semi-colons.” [1]
> “Structured Programming supports the law of the excluded muddle.” [1]
> [1]: [Epigrams on Programming — Alan J. — P. Yale University]

Yes... you caught me in a case of typing too fast and not proofreading.