Class wide preconditions: error in GNAT implementation?

Class wide preconditions: error in GNAT implementation?

[ytomino]

Hello.
I read https://groups.google.com/d/topic/comp.lang.ada/03cKrGghF2Y/discussion and recall a related question.

See below example:

package preconds is
   package Tools is
      function Write_In_Expr (S : String) return Boolean; -- Put_Line (S) and return True
   end Tools;
   package As is
      type A is tagged null record;
      procedure foo (Object : A) -- empty body
         with Pre'Class => Tools.Write_In_Expr ("A, in!"),
              Post'Class => Tools.Write_In_Expr ("A, out!");
   end As;
   package Bs is
      type B is new As.A with null record;
      overriding procedure foo (Object : B) -- empty body
         with Pre'Class  => Tools.Write_In_Expr ("B, in!"), -- [*]
              Post'Class => Tools.Write_In_Expr ("B, out!");
   end Bs;
end preconds;

with preconds; use preconds;
procedure precondmain is
   x : access As.A'Class := new Bs.B;
begin
   As.foo (x.all); -- dispatching call as A'Class
end precondmain;

% gnatmake -gnat2012 -gnata precondmain.adb
% ./precondmain
B, in!
B, out!
A, out!

And change [*] to Pre'Class => Tools.Write_In_Expr ("B, in!") and False,

% gnatmake -gnat2012 -gnata precondmain.adb
% ./precondmain                            
B, in!
A, in!
B, out!
A, out!

It seems that the preconditions were evaluated as pragma Assert (B'Pre'Class and then A'Pre'Class);

By the way, AARM 6.1.1 38.a/3-b/3 says

> Ramification: For a dispatching call, we are talking about the Pre'Class(es) that apply to the subprogram that the dispatching call is resolving to, not the Pre'Class(es) for the subprogram that is ultimately dispatched to. The class-wide precondition of the resolved call is necessarily the same or stronger than that of the invoked call. For a statically bound call, these are the same; for an access-to-subprogram, (which has no class-wide preconditions of its own), we check the class-wide preconditions of the invoked routine. 

>Implementation Note: These rules imply that logically, class-wide preconditions of routines must be checked at the point of call (other than for access-to-subprogram calls, which must be checked in the body, probably using a wrapper). Specific preconditions that might be called with a dispatching call or via an access-to-subprogram value must be checked inside of the subprogram body. In contrast, the postcondition checks always need to be checked inside the body of the routine. Of course, an implementation can evaluate all of these at the point of call for statically bound calls if the implementation uses wrappers for dispatching bodies and for 'Access values.

I think(hope), this two lines mean only A'Pre'Class should be evaluated in this case.

B'Pre'Class should not be evaluated in this case. Isn't it?

P.S. dmd (D language compiler) had same error. Its discussion may help for reference.
http://d.puremagic.com/issues/show_bug.cgi?id=6857

Re: Class wide preconditions: error in GNAT implementation?

[Georg Bauhaus]

On 15.02.13 04:55, ytomino wrote:
> See below example:

This yields an ICE for me:

gcc -c -gnata -gnat2012 -gnatd.n -gnatG -gnatl preconds.ads
/Users/bauhaus/mine/lib/gcc/x86_64-apple-darwin11.4.2/4.8.0/adainclude/system.ads

GNAT 4.8.0 20130212 (experimental) [trunk revision 195968]
Copyright 1992-2013, Free Software Foundation, Inc.
preconds.ads
/Users/bauhaus/mine/lib/gcc/x86_64-apple-darwin11.4.2/4.8.0/adainclude/a-tags.ads
/Users/bauhaus/mine/lib/gcc/x86_64-apple-darwin11.4.2/4.8.0/adainclude/ada.ads
/Users/bauhaus/mine/lib/gcc/x86_64-apple-darwin11.4.2/4.8.0/adainclude/s-stoele.ads
/Users/bauhaus/mine/lib/gcc/x86_64-apple-darwin11.4.2/4.8.0/adainclude/s-stoele.adb
/Users/bauhaus/mine/lib/gcc/x86_64-apple-darwin11.4.2/4.8.0/adainclude/a-unccon.ads
/Users/bauhaus/mine/lib/gcc/x86_64-apple-darwin11.4.2/4.8.0/adainclude/s-stalib.ads
/Users/bauhaus/mine/lib/gcc/x86_64-apple-darwin11.4.2/4.8.0/adainclude/s-exctab.ads
+===========================GNAT BUG DETECTED==============================+
| 4.8.0 20130212 (experimental) [trunk revision 195968] (x86_64-apple-darwin11.4.2) |
| Assert_Failure atree.adb:903                                             |
| Error detected at preconds.ads:5:4                                       |
| Please submit a bug report; see http://gcc.gnu.org/bugs.html.            |
| Use a subject line meaningful to you and us to track the bug.            |
| Include the entire contents of this bug box in the report.               |
| Include the exact gcc or gnatmake command that you entered.              |
| Also include sources listed below in gnatchop format                     |
| (concatenated together with no headers between files).                   |
+==========================================================================+

Please include these source files with error report
Note that list may not be accurate in some cases,
so please double check that the problem can still
be reproduced with the set of files listed.
Consider also -gnatd.n switch (see debug.adb).

preconds.ads

Source recreated from tree for preconds (spec)
----------------------------------------------

with ada.tags;

package preconds is

    package tools is
       function write_in_expr (s : string) return boolean;
    end tools;

    package as is
       type a is tagged null record;
       procedure foo (object : a)
         with pre'Class => tools.write_in_expr ("A, in!"),
              post'Class => tools.write_in_expr ("A, out!");
       pragma postcondition (check => tools.write_in_expr ("A, out!"),
         message => "failed postcondition from preconds.ads:9");
       pragma precondition (check => tools.write_in_expr ("A, in!"),
         message => "failed precondition from preconds.ads:8");
    end as;

    package bs is
       type b is new as.a with null record;
       procedure foo (object : b)
         with pre'Class => tools.write_in_expr ("B, in!"),
              post'Class => tools.write_in_expr ("B, out!");
    end bs;
end preconds;



Compiling: preconds.ads (source file time stamp: 2013-02-15 10:13:22)

      1. package preconds is
      2.    package Tools is
      3.       function Write_In_Expr (S : String) return Boolean; -- Put_Line (S) and return True
      4.    end Tools;
      5.    package As is
      6.       type A is tagged null record;
      7.       procedure foo (Object : A) -- empty body
      8.          with Pre'Class => Tools.Write_In_Expr ("A, in!"),
      9.               Post'Class => Tools.Write_In_Expr ("A, out!");
     10.    end As;
     11.    package Bs is
     12.       type B is new As.A with null record;
     13.       overriding procedure foo (Object : B) -- empty body
     14.          with Pre'Class  => Tools.Write_In_Expr ("B, in!"), -- [*]
     15.               Post'Class => Tools.Write_In_Expr ("B, out!");
     16.    end Bs;
     17. end preconds;

  17 lines: No errors
compilation abandoned
Source recreated from tree for preconds (spec)
----------------------------------------------

with ada.tags;

package preconds is

    package tools is
       function write_in_expr (s : string) return boolean;
    end tools;

    package as is
       type a is tagged null record;
       procedure foo (object : a)
         with pre'Class => tools.write_in_expr ("A, in!"),
              post'Class => tools.write_in_expr ("A, out!");
       pragma postcondition (check => tools.write_in_expr ("A, out!"),
         message => "failed postcondition from preconds.ads:9");
       pragma precondition (check => tools.write_in_expr ("A, in!"),
         message => "failed precondition from preconds.ads:8");
    end as;

    package bs is
       type b is new as.a with null record;
       procedure foo (object : b)
         with pre'Class => tools.write_in_expr ("B, in!"),
              post'Class => tools.write_in_expr ("B, out!");
    end bs;
end preconds;

gnatmake: "preconds.ads" compilation error

Re: Class wide preconditions: error in GNAT implementation?

[ytomino]

On Friday, February 15, 2013 7:15:13 PM UTC+9, Georg Bauhaus wrote:
> This yields an ICE for me:

Ah, yes. My gcc-4.7.2 reports same ICE.
But gcc-4.6.3 and GNAT GPL 2012 can compile it.

Re: Class wide preconditions: error in GNAT implementation?

[Randy Brukardt]

"ytomino" <aghia05@gmail.com> wrote in message 
news:e155e2d6-ba1f-4fc0-a6e3-dafde002670b@googlegroups.com...
...
>% gnatmake -gnat2012 -gnata precondmain.adb
>% ./precondmain
>B, in!
>B, out!
>A, out!
>
>And change [*] to Pre'Class => Tools.Write_In_Expr ("B, in!") and False,
>
>% gnatmake -gnat2012 -gnata precondmain.adb
>% ./precondmain
>B, in!
>A, in!
>B, out!
>A, out!

This looks right to me (well, actually not quite, see far below).

>It seems that the preconditions were evaluated as pragma Assert 
>(B'Pre'Class and then A'Pre'Class);

Class-wide Preconditions are combined with "or", not "and". And of course 
Once you get True for "or", you don't need to evaluate any more of them. See 
6.1.1(33/3)- "if and only if all ... evaluated to False".

The order of evaluation of these expressions is unspecified, so which one 
gets evaluated depends on the compiler.

Postconditions (and specific preconditions) are combined with "and".

The reasons for this are found in the theories of LSP. I could explain it, 
but it would take me all day, and you'd probably be more confused than you 
started. :-) (It took a long time for most of the ARG, me included, to 
understand this well enough to determine whether or not the features were 
properly defined.)

OTOH, I didn't realize that you had a dispatching call. In that case, the 
precondition is supposed to just be the Pre'Class for A, which is stronger 
that A or B which a direct call would use. Probably GNAT dispatched and then 
checked the precondition. Technically, that's wrong (although I would have a 
hard time caring, the reason for the stronger precondition on dispatching 
calls is to allow analysis without knowing the actual tag, it doesn't have 
anything to do with correctness).

                                 Randy.

Re: Class wide preconditions: error in GNAT implementation?

[ytomino]

On Saturday, February 16, 2013 10:01:53 AM UTC+9, Randy Brukardt wrote:
> This looks right to me (well, actually not quite, see far below).
> >It seems that the preconditions were evaluated as pragma Assert 
> >(B'Pre'Class and then A'Pre'Class);
> 
> Class-wide Preconditions are combined with "or", not "and". And of course 
> Once you get True for "or", you don't need to evaluate any more of them. See 
> 6.1.1(33/3)- "if and only if all ... evaluated to False".
> The order of evaluation of these expressions is unspecified, so which one 
> gets evaluated depends on the compiler.
> 
> Postconditions (and specific preconditions) are combined with "and".
> 
> The reasons for this are found in the theories of LSP. I could explain it, 
> but it would take me all day, and you'd probably be more confused than you 
> started. :-) (It took a long time for most of the ARG, me included, to 
> understand this well enough to determine whether or not the features were 
> properly defined.)

Oh! Sorry, you are right at this point. 
That's evaluated as pragma Assert (B'Pre'Class or else A'Pre'Class); 
I had a mistake in writing.

I really wanted to talk about the treatment of Pre'Class in dispatching call.

> OTOH, I didn't realize that you had a dispatching call. In that case, the 
> precondition is supposed to just be the Pre'Class for A, which is stronger 
> that A or B which a direct call would use. Probably GNAT dispatched and then 
> checked the precondition. Technically, that's wrong

Yes. GNAT inserts Pre'Class into function body.
AARM 6.1.1 38.a/3-b/3 indicates, if my understanding is right,
Pre'Class should be evaluated after parameters are evaluated and before dispatching.

> (although I would have a 
> hard time caring, the reason for the stronger precondition on dispatching 
> calls is to allow analysis without knowing the actual tag, it doesn't have 
> anything to do with correctness).

No. It's related to correctness. Precondition is a promise for caller, not callee.
In this case, the caller should keep As.foo'Pre'Class because calling As.foo.

This rule specified by AARM is agreement with the conclusion of the discussion
of D language and explained in Eiffel.

I read the Eiffel book "Object-Oriented Software Construction 2/E" and this part of AARM
again and again when I knew the error of dmd on last year.
At that time, I had been contented because AARM seems right for me.

But, this behavior of GNAT is completely the same as dmd concluded that had a bug.

Re: Class wide preconditions: error in GNAT implementation?

[Dmitry A. Kazakov]

On Fri, 15 Feb 2013 18:50:36 -0800 (PST), ytomino wrote:

> No. It's related to correctness.

Not when checked dynamically by the same program.

> Precondition is a promise for caller, not callee.

Actually it is imposed on both.

> In this case, the caller should keep As.foo'Pre'Class because calling As.foo.

No, the caller shall satisfy the precondition of the callee. Regarding
inheritance, a primitive operation (callee) may weaken the precondition it
overrides. This is why logical disjunction apply, as Randy said.
Considering individual terms of the disjunction, the caller is allowed to
satisfy at least one of them to make the call valid.

Note that if the callee were a class-wide operation then its precondition
would read literally.

P.S. To make the model working especially with multiple-dispatch, pre- and
post-conditions should be stated for individual arguments and the result(s)
rather than on the operation as a whole. The same operation could
(theoretically) be primitive and non-primitive in its different arguments.
The rule of weakening preconditions and strengthening post-conditions apply
per argument/result inheritance path.

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

Re: Class wide preconditions: error in GNAT implementation?

[ytomino]

We are already inured to polymorphism. So this fact counters to our intuition.
I had been confused when I knew it. After all, I took a Eiffel book out.

On Saturday, February 16, 2013 6:28:10 PM UTC+9, Dmitry A. Kazakov wrote:
> On Fri, 15 Feb 2013 18:50:36 -0800 (PST), ytomino wrote:
> > No. It's related to correctness.
> Not when checked dynamically by the same program.
> > Precondition is a promise for caller, not callee.
> Actually it is imposed on both.

No. Precondition is imposed on only caller.

> > In this case, the caller should keep As.foo'Pre'Class because calling As.foo.
> No, the caller shall satisfy the precondition of the callee. Regarding
> inheritance, a primitive operation (callee) may weaken the precondition it
> overrides. This is why logical disjunction apply, as Randy said.

No. The caller is "client" of not Bs but As, in this case.

> Considering individual terms of the disjunction, the caller is allowed to
> satisfy at least one of them to make the call valid.

Imagine, the system is running correctly, but depending on weak precondition of the subclass.
On day, new subclass is introduced into this system.
This new subclass has strong precondition equally to the superclass.
But, existing callers is depending on weak one.
It's a bug of callers, not subclasses.

"Client" code of superclass should have been fully keeping precondition of superclass all along.

In "Design by Contact", the caller of superclass has a contract with only superclass.
Randy wrote "to allow analysis without knowing the actual tag".
This word is applied to not only analyzer machine but also human programmers.

> Note that if the callee were a class-wide operation then its precondition
> would read literally.

Of course.

If you had time, please read the discussion in http://d.puremagic.com/issues/show_bug.cgi?id=6857 .
Maybe it's more easy to understand than my words.

Re: Class wide preconditions: error in GNAT implementation?

[Georg Bauhaus]

On 16.02.13 10:28, Dmitry A. Kazakov wrote:
> On Fri, 15 Feb 2013 18:50:36 -0800 (PST), ytomino wrote:
>
>> No. It's related to correctness.
>
> Not when checked dynamically by the same program.

"To be related to correctness" is not the same as "a correct proof
of correctness" (if such can exist for programs in general).

Re: Class wide preconditions: error in GNAT implementation?

[Dmitry A. Kazakov]

On Sat, 16 Feb 2013 05:13:53 -0800 (PST), ytomino wrote:

>>> In this case, the caller should keep As.foo'Pre'Class because calling As.foo.
>> No, the caller shall satisfy the precondition of the callee. Regarding
>> inheritance, a primitive operation (callee) may weaken the precondition it
>> overrides. This is why logical disjunction apply, as Randy said.
> 
> No. The caller is "client" of not Bs but As, in this case.

The precondition of a dispatching call is one of the class. The
precondition of the specific operation can be weaker. The precondition of a
LSP subclass can be stronger. All three shall be satisfied by the caller,
but only the first one is actually constraining for it, because the second
two are automatically satisfied through the mechanism of dispatching call
and type coercion.

>> Considering individual terms of the disjunction, the caller is allowed to
>> satisfy at least one of them to make the call valid.
> 
> Imagine, the system is running correctly, but depending on weak precondition of the subclass.
> On day, new subclass is introduced into this system.
> This new subclass has strong precondition equally to the superclass.
> But, existing callers is depending on weak one.
> It's a bug of callers, not subclasses.

It won't happen. A weakened precondition apply to the another caller, an
imaginary polymorphic body which is called by the original caller. When you
arrive into that body and go trough the tag-case, and are ready to call the
specific body, then the precondition of the latter apply. Original caller
has to satisfy the precondition of the operation it calls. For a
dispatching operation it is one of the class.

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

Re: Class wide preconditions: error in GNAT implementation?

[ytomino]

On Sunday, February 17, 2013 1:35:12 AM UTC+9, Dmitry A. Kazakov wrote:
> On Sat, 16 Feb 2013 05:13:53 -0800 (PST), ytomino wrote:
> >>> In this case, the caller should keep As.foo'Pre'Class because calling As.foo.
> >> No, the caller shall satisfy the precondition of the callee. Regarding
> >> inheritance, a primitive operation (callee) may weaken the precondition it
> >> overrides. This is why logical disjunction apply, as Randy said.
> > No. The caller is "client" of not Bs but As, in this case.
> 
> The precondition of a dispatching call is one of the class. The
> precondition of the specific operation can be weaker. The precondition of a
> LSP subclass can be stronger. All three shall be satisfied by the caller,
> but only the first one is actually constraining for it, because the second
> two are automatically satisfied through the mechanism of dispatching call
> and type coercion.

Yes. *only the first one* = only As.foo'Pre'Class should be satisfied.

> >> Considering individual terms of the disjunction, the caller is allowed to
> >> satisfy at least one of them to make the call valid.
> > Imagine, the system is running correctly, but depending on weak precondition of the subclass.
> > On day, new subclass is introduced into this system.
> > This new subclass has strong precondition equally to the superclass.
> > But, existing callers is depending on weak one.
> > It's a bug of callers, not subclasses.
> 
> It won't happen. A weakened precondition apply to the another caller, an
> imaginary polymorphic body which is called by the original caller. When you
> arrive into that body and go trough the tag-case, and are ready to call the
> specific body, then the precondition of the latter apply. Original caller
> has to satisfy the precondition of the operation it calls. For a
> dispatching operation it is one of the class.

Are you imagining the dispatcher like below?

procedure foo_Dispatcher (Object : A'Class) is
begin
   pragma Assert (As.foo'Pre'Class);
   case Object'Tag is
      when A'Tag =>
         As.foo (A (Object));
      when B'Tag =>
         pragma Assert (Bs.foo'Pre'Class); -- unnecessary because weaker
         Bs.foo (B (Object));
      ...
   end case;
end foo_Dispatcher;

If it is, your understanding is same as mine.

I'll repeat what I said. I believe the specification in Ada RM(AARM) is right
and merely point out the error in the behavior of GNAT.
The behavior of GNAT is different from what you says.

Re: Class wide preconditions: error in GNAT implementation?

[Simon Wright]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> OTOH, I didn't realize that you had a dispatching call. In that case,
> the precondition is supposed to just be the Pre'Class for A, which is
> stronger that A or B which a direct call would use. Probably GNAT
> dispatched and then checked the precondition. Technically, that's
> wrong (although I would have a hard time caring, the reason for the
> stronger precondition on dispatching calls is to allow analysis
> without knowing the actual tag, it doesn't have anything to do with
> correctness).

I think that the rule that GNAT appears to be breaking is 6.6.1(38)[1]?

I've constructed an example where GNAT's behaviour results in caller
code that used to work (with checks enabled) no longer working,
depending on the actual type for a classwide (an access-to-classwide,
as might be used if say the application logger could be changed at run
time):

with Ada.Exceptions; use Ada.Exceptions;
with Ada.Text_IO; use Ada.Text_IO;

procedure Conditions is

   package A_Pack is
      type T is tagged null record;
      not overriding
      procedure P (This : T; Var : Integer) is null
        with Pre'Class => Var >= 1;
   end A_Pack;

   package B_Pack is
      type T is new A_Pack.T with null record;
      overriding
      procedure P (This : T; Var : Integer) is null
        with Pre'Class => Var >= 0;                -- widening
   end B_Pack;

   package C_Pack is
      type T is new A_Pack.T with null record;
      overriding
      procedure P (This : T; Var : Integer) is null;
   end C_Pack;

begin

   declare
      O : access A_Pack.T'Class;
   begin
      O := new B_Pack.T;
      Put_Line ("passing 0 to an actual B_Pack.T");
      O.P (0);
      Put_Line ("success.");
      O := new C_Pack.T;
      Put_Line ("passing 0 to an actual C_Pack.T");
      O.P (0);
      Put_Line ("success.");
   exception
      when E : others =>
         Put_Line (Exception_Information (E));
   end;

end Conditions;

and the output is

$ ./conditions 
passing 0 to an actual B_Pack.T
success.
passing 0 to an actual C_Pack.T
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed inherited precondition from conditions.adb:10


[1] http://www.ada-auth.org/standards/12aarm/html/AA-6-1-1.html#p38

Re: Class wide preconditions: error in GNAT implementation?

[ytomino]

Replace precondition of Bs.foo for a clarification.

>          pragma Assert (Bs.foo'Pre'Class); -- unnecessary because weaker 
>          Bs.foo (B (Object)); 

pragma Assert (As.foo'Pre'Class or else Bs.foo'Pre'Class); -- unnecessary because weaker 
Bs.foo (B (Object)); 

Re: Class wide preconditions: error in GNAT implementation?

[ytomino]

I am not aware of the intention of the writer of AARM (Randy?).
Though as far as I read AARM and compare it with the Eiffel book,

>      O := new B_Pack.T; 
>      Put_Line ("passing 0 to an actual B_Pack.T"); 
>      O.P (0); 

Calling B_Pack.P via access A_Pack.T'Class should be failure.

6.6.1.38.a/3:

> Pre'Class(es) that apply to the subprogram that the dispatching call
> is resolving to, not the Pre'Class(es) for the subprogram that is
> ultimately dispatched to. 

"resolving to" = A_Pack.P
"dispatched to" = B_Pack.P

And, this rule is correspond to page 575 of
"Object-Oriented Software Construction 2/E". It indicates that
the caller (client) of A_Pack.T('Class) has only contract with A_Pack.T.
If the caller want to use weaker contract, the caller should become 
a direct client of B_Pack.T.

The photo of this page has been uploaded in the discussion of dmd:
http://d.puremagic.com/issues/show_bug.cgi?id=6857#c84

Re: Class wide preconditions: error in GNAT implementation?

[Dmitry A. Kazakov]

On Sat, 16 Feb 2013 11:55:55 -0800 (PST), ytomino wrote:

> On Sunday, February 17, 2013 1:35:12 AM UTC+9, Dmitry A. Kazakov wrote:
>> On Sat, 16 Feb 2013 05:13:53 -0800 (PST), ytomino wrote:
>>>>> In this case, the caller should keep As.foo'Pre'Class because calling As.foo.
>>>> No, the caller shall satisfy the precondition of the callee. Regarding
>>>> inheritance, a primitive operation (callee) may weaken the precondition it
>>>> overrides. This is why logical disjunction apply, as Randy said.
>>> No. The caller is "client" of not Bs but As, in this case.
>> 
>> The precondition of a dispatching call is one of the class. The
>> precondition of the specific operation can be weaker. The precondition of a
>> LSP subclass can be stronger. All three shall be satisfied by the caller,
>> but only the first one is actually constraining for it, because the second
>> two are automatically satisfied through the mechanism of dispatching call
>> and type coercion.
> 
> Yes. *only the first one* = only As.foo'Pre'Class should be satisfied.

No, all preconditions must be satisfied, otherwise, the program is
incorrect, provided it is correctness we are talking about.

>>>> Considering individual terms of the disjunction, the caller is allowed to
>>>> satisfy at least one of them to make the call valid.
>>> Imagine, the system is running correctly, but depending on weak precondition of the subclass.
>>> On day, new subclass is introduced into this system.
>>> This new subclass has strong precondition equally to the superclass.
>>> But, existing callers is depending on weak one.
>>> It's a bug of callers, not subclasses.
>> 
>> It won't happen. A weakened precondition apply to the another caller, an
>> imaginary polymorphic body which is called by the original caller. When you
>> arrive into that body and go trough the tag-case, and are ready to call the
>> specific body, then the precondition of the latter apply. Original caller
>> has to satisfy the precondition of the operation it calls. For a
>> dispatching operation it is one of the class.
> 
> Are you imagining the dispatcher like below?
> 
> procedure foo_Dispatcher (Object : A'Class) is
> begin
>    pragma Assert (As.foo'Pre'Class);
>    case Object'Tag is
>       when A'Tag =>
>          As.foo (A (Object));
>       when B'Tag =>
>          pragma Assert (Bs.foo'Pre'Class); -- unnecessary because weaker
>          Bs.foo (B (Object));
>       ...
>    end case;
> end foo_Dispatcher;
> 
> If it is, your understanding is same as mine.

But then the precondition of B'Class is *required* to be true for an object
which is in that class. The precondition of A'Class is weaker and need not
to be checked if one for B'Class is satisfied.

> I'll repeat what I said. I believe the specification in Ada RM(AARM) is right
> and merely point out the error in the behavior of GNAT.
> The behavior of GNAT is different from what you says.

I don't know. From the POV of correctness check, GNAT's behavior is
perfectly OK. This only shows how dangerous it is to confuse checks with
program semantics.

Any program that rely on an outcome of a correctness check is automatically
illegal. Yours already is since it prints from "checks."

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

Re: Class wide preconditions: error in GNAT implementation?

[Simon Wright]

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

> On Sat, 16 Feb 2013 11:55:55 -0800 (PST), ytomino wrote:
>
>> On Sunday, February 17, 2013 1:35:12 AM UTC+9, Dmitry A. Kazakov wrote:
>>> On Sat, 16 Feb 2013 05:13:53 -0800 (PST), ytomino wrote:
>>>>>> In this case, the caller should keep As.foo'Pre'Class because
>>>>> calling As.foo.
>>>>> No, the caller shall satisfy the precondition of the
>>>>> callee. Regarding inheritance, a primitive operation (callee) may
>>>>> weaken the precondition it overrides. This is why logical
>>>>> disjunction apply, as Randy said.
>>>> No. The caller is "client" of not Bs but As, in this case.
>>> 
>>> The precondition of a dispatching call is one of the class. The
>>> precondition of the specific operation can be weaker. The
>>> precondition of a LSP subclass can be stronger. All three shall be
>>> satisfied by the caller, but only the first one is actually
>>> constraining for it, because the second two are automatically
>>> satisfied through the mechanism of dispatching call and type
>>> coercion.
>> 
>> Yes. *only the first one* = only As.foo'Pre'Class should be satisfied.
>
> No, all preconditions must be satisfied, otherwise, the program is
> incorrect, provided it is correctness we are talking about.
[...]
> But then the precondition of B'Class is *required* to be true for an
> object which is in that class. The precondition of A'Class is weaker
> and need not to be checked if one for B'Class is satisfied.

This is the wrong way round. A subclass can only _weaken_ the
precondition of the superclass. Anything else violates LSP.

This new feature introduces a whole new opportunity for error: getting
the preconditions wrong.

Re: Class wide preconditions: error in GNAT implementation?

[Dmitry A. Kazakov]

On Mon, 18 Feb 2013 09:17:57 +0000, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Sat, 16 Feb 2013 11:55:55 -0800 (PST), ytomino wrote:
>>
>>> On Sunday, February 17, 2013 1:35:12 AM UTC+9, Dmitry A. Kazakov wrote:
>>>> On Sat, 16 Feb 2013 05:13:53 -0800 (PST), ytomino wrote:
>>>>>>> In this case, the caller should keep As.foo'Pre'Class because
>>>>>> calling As.foo.
>>>>>> No, the caller shall satisfy the precondition of the
>>>>>> callee. Regarding inheritance, a primitive operation (callee) may
>>>>>> weaken the precondition it overrides. This is why logical
>>>>>> disjunction apply, as Randy said.
>>>>> No. The caller is "client" of not Bs but As, in this case.
>>>> 
>>>> The precondition of a dispatching call is one of the class. The
>>>> precondition of the specific operation can be weaker. The
>>>> precondition of a LSP subclass can be stronger. All three shall be
>>>> satisfied by the caller, but only the first one is actually
>>>> constraining for it, because the second two are automatically
>>>> satisfied through the mechanism of dispatching call and type
>>>> coercion.
>>> 
>>> Yes. *only the first one* = only As.foo'Pre'Class should be satisfied.
>>
>> No, all preconditions must be satisfied, otherwise, the program is
>> incorrect, provided it is correctness we are talking about.
> [...]
>> But then the precondition of B'Class is *required* to be true for an
>> object which is in that class. The precondition of A'Class is weaker
>> and need not to be checked if one for B'Class is satisfied.
> 
> This is the wrong way round. A subclass can only _weaken_ the
> precondition of the superclass. Anything else violates LSP.

LSP is wrong in general. A narrower "truer" version of LSP applies
specifically to operations and their preconditions and all that in the
context of substitutability, which is not the case for a dispatching call.
A dispatching call does not substitute unless the body is inherited.

Anyway, trivially, consider the following types:

   type A is ...;
   type B is new A with ...;

The predicate P=x in A'Class is true for both A and B. The predicate Q=y in
B'Class is true B and false for A. hence Q=>P, Q is stronger.

[Tag checks violate LSP]

> This new feature introduces a whole new opportunity for error: getting
> the preconditions wrong.

Yes, but the major crime here is mingling correctness with program
semantics. The thing meant to be executed in the prologue of an operation
has nothing to do with correctness, it is about operation composition upon
inheritance and/or about object construction.

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

Re: Class wide preconditions: error in GNAT implementation?

[Simon Wright]

ytomino <aghia05@gmail.com> writes:

> I am not aware of the intention of the writer of AARM (Randy?).
> Though as far as I read AARM and compare it with the Eiffel book,
>
>>      O := new B_Pack.T; 
>>      Put_Line ("passing 0 to an actual B_Pack.T"); 
>>      O.P (0); 
>
> Calling B_Pack.P via access A_Pack.T'Class should be failure.
>
> 6.6.1.38.a/3:
>
>> Pre'Class(es) that apply to the subprogram that the dispatching call
>> is resolving to, not the Pre'Class(es) for the subprogram that is
>> ultimately dispatched to. 
>
> "resolving to" = A_Pack.P
> "dispatched to" = B_Pack.P

Exactly so; both calls should have failed.

Re: Class wide preconditions: error in GNAT implementation?

[Simon Wright]

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

> On Mon, 18 Feb 2013 09:17:57 +0000, Simon Wright wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>> 
>>> But then the precondition of B'Class is *required* to be true for an
>>> object which is in that class. The precondition of A'Class is weaker
>>> and need not to be checked if one for B'Class is satisfied.
>> 
>> This is the wrong way round. A subclass can only _weaken_ the
>> precondition of the superclass. Anything else violates LSP.
>
> LSP is wrong in general.

Is there a Kazakov Substitution Principle, then? (or someone else's ...)

> Anyway, trivially, consider the following types:
>
>    type A is ...;
>    type B is new A with ...;
>
> The predicate P=x in A'Class is true for both A and B. The predicate
> Q=y in B'Class is true B and false for A. hence Q=>P, Q is stronger.

If you allow code like this, how can you draw any conclusions about the
correctness of a call through a pointer to A'Class? No problem if you
don't have any class-wide calls, but you've just eliminated dispatching.

> [Tag checks violate LSP]

Don't understand.

>> This new feature introduces a whole new opportunity for error:
>> getting the preconditions wrong.
>
> Yes, but the major crime here is mingling correctness with program
> semantics. The thing meant to be executed in the prologue of an
> operation has nothing to do with correctness, it is about operation
> composition upon inheritance and/or about object construction.

The intention is (AIUI) to be able to extract {pre,post}conditions from
an Ada program and do static verification; how is what Ada2012 does
(dynamically) incompatible with that?

Re: Class wide preconditions: error in GNAT implementation?

[ytomino]

On Tuesday, February 19, 2013 2:49:58 AM UTC+9, Simon Wright wrote:
> Exactly so; both calls should have failed.

That is so. Thank you!

(Honestly, like timon.gehr and others did, I expected that it's more hard to have someone understand this.
My fear was utterly groundless.)

Re: Class wide preconditions: error in GNAT implementation?

[ytomino]

On Monday, February 18, 2013 5:30:16 PM UTC+9, Dmitry A. Kazakov wrote:
> No, all preconditions must be satisfied, otherwise, the program is
> incorrect, provided it is correctness we are talking about.
> 
> But then the precondition of B'Class is *required* to be true for an object
> which is in that class. The precondition of A'Class is weaker and need not
> to be checked if one for B'Class is satisfied.

Excuse me for misunderstanding your opinion.

But, do you have the same mistake as mine in the first post?
Preconditions are combined by "or else".
Therefore, increasing its conditions means making it weaker.

Re: Class wide preconditions: error in GNAT implementation?

[Dmitry A. Kazakov]

On Mon, 18 Feb 2013 18:04:53 +0000, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Mon, 18 Feb 2013 09:17:57 +0000, Simon Wright wrote:
>>
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>>> 
>>>> But then the precondition of B'Class is *required* to be true for an
>>>> object which is in that class. The precondition of A'Class is weaker
>>>> and need not to be checked if one for B'Class is satisfied.
>>> 
>>> This is the wrong way round. A subclass can only _weaken_ the
>>> precondition of the superclass. Anything else violates LSP.
>>
>> LSP is wrong in general.
> 
> Is there a Kazakov Substitution Principle, then? (or someone else's ...)

You can find it all around Ada. E.g. constants, in-parameters, subtypes are
examples of subtypes violating LSP.

Ada's substitutability principle is that anything is substitutable that is
not rejected by the compiler. (:-))

Liskov's motivation was to coin subtyping in terms of substitutability.
This is impossible to do without limiting the context of substitution. A
type system cannot be based on LSP, unfortunately.

>> Anyway, trivially, consider the following types:
>>
>>    type A is ...;
>>    type B is new A with ...;
>>
>> The predicate P=x in A'Class is true for both A and B. The predicate
>> Q=y in B'Class is true B and false for A. hence Q=>P, Q is stronger.
> 
> If you allow code like this, how can you draw any conclusions about the
> correctness of a call through a pointer to A'Class?

Do you believe in correctness proofs without looking into the bodies?

>> [Tag checks violate LSP]
> 
> Don't understand.

Because these could be used to construct predicates which would depend on
the actual type. Absolute substitutability as required by "naive"
interpretations of LSP is based on types being absolutely indistinguishable
for the clients, which tags obviously defeat.

>>> This new feature introduces a whole new opportunity for error:
>>> getting the preconditions wrong.
>>
>> Yes, but the major crime here is mingling correctness with program
>> semantics. The thing meant to be executed in the prologue of an
>> operation has nothing to do with correctness, it is about operation
>> composition upon inheritance and/or about object construction.
> 
> The intention is (AIUI) to be able to extract {pre,post}conditions from
> an Ada program and do static verification; how is what Ada2012 does
> (dynamically) incompatible with that?

Per observation that static /= dynamic.

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

Re: Class wide preconditions: error in GNAT implementation?

[Dmitry A. Kazakov]

On Mon, 18 Feb 2013 11:02:31 -0800 (PST), ytomino wrote:

> On Monday, February 18, 2013 5:30:16 PM UTC+9, Dmitry A. Kazakov wrote:
>> No, all preconditions must be satisfied, otherwise, the program is
>> incorrect, provided it is correctness we are talking about.
>> 
>> But then the precondition of B'Class is *required* to be true for an object
>> which is in that class. The precondition of A'Class is weaker and need not
>> to be checked if one for B'Class is satisfied.
> 
> Excuse me for misunderstanding your opinion.
> 
> But, do you have the same mistake as mine in�the first post?
> Preconditions are combined by "or else".

That depends on what you do with the set of values at hand and what the
terms being combined mean. If you narrow the set, then obviously the
precondition strengthens which could mean "and" for the terms associated
with independent subsets of values. If you widen the set it could be "or."
It could be anything in more complex cases when subsets are not independent
or when some values are added and some are removed, when some operations
are in, some are out and some are inout. etc.

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

Re: Class wide preconditions: error in GNAT implementation?

[Simon Wright]

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

> On Mon, 18 Feb 2013 18:04:53 +0000, Simon Wright wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>> 

>>> Anyway, trivially, consider the following types:
>>>
>>>    type A is ...;
>>>    type B is new A with ...;
>>>
>>> The predicate P=x in A'Class is true for both A and B. The predicate
>>> Q=y in B'Class is true B and false for A. hence Q=>P, Q is stronger.
>> 
>> If you allow code like this, how can you draw any conclusions about the
>> correctness of a call through a pointer to A'Class?
>
> Do you believe in correctness proofs without looking into the bodies?

Well, you've consructed a situation which is plainly wrong if we're
going to be talking substitutablity.

I would expect that if you could prove that

  * all calls via A'Class meet A's precondition; and

  * all derived type implementations produce valid output when given
    parameters that meet A's precondition

then you'd be a long way toward a correctness proof.

>>> [Tag checks violate LSP]
>> 
>> Don't understand.
>
> Because these could be used to construct predicates which would depend
> on the actual type. Absolute substitutability as required by "naive"
> interpretations of LSP is based on types being absolutely
> indistinguishable for the clients, which tags obviously defeat.

Then don't write predicates like that! (and slap the wrist of anyone you
find doing it).

Re: Class wide preconditions: error in GNAT implementation?

[Dmitry A. Kazakov]

On Mon, 18 Feb 2013 20:42:56 +0000, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Mon, 18 Feb 2013 18:04:53 +0000, Simon Wright wrote:
>>
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>>>> Anyway, trivially, consider the following types:
>>>>
>>>>    type A is ...;
>>>>    type B is new A with ...;
>>>>
>>>> The predicate P=x in A'Class is true for both A and B. The predicate
>>>> Q=y in B'Class is true B and false for A. hence Q=>P, Q is stronger.
>>> 
>>> If you allow code like this, how can you draw any conclusions about the
>>> correctness of a call through a pointer to A'Class?
>>
>> Do you believe in correctness proofs without looking into the bodies?
> 
> Well, you've consructed a situation which is plainly wrong if we're
> going to be talking substitutablity.

But that is not same as correctness. Even if substitutability were
decidable that would not ensure correctness. And conversely a program can
be correct even with substitutability violated.

> I would expect that if you could prove that
> 
>   * all calls via A'Class meet A's precondition; and
> 
>   * all derived type implementations produce valid output when given
>     parameters that meet A's precondition
> 
> then you'd be a long way toward a correctness proof.

The first is trivial, the second is undecidable.

>>>> [Tag checks violate LSP]
>>> 
>>> Don't understand.
>>
>> Because these could be used to construct predicates which would depend
>> on the actual type. Absolute substitutability as required by "naive"
>> interpretations of LSP is based on types being absolutely
>> indistinguishable for the clients, which tags obviously defeat.
> 
> Then don't write predicates like that! (and slap the wrist of anyone you
> find doing it).

But the idea of LSP (behavioral notion of subtype) was to prevent such
predicates coming into existence per construction of subtypes. The sad
reality is that we need them to make our programs working, e.g. for
dispatching. Mere existence of predicates which do not hold upon subtyping
does not make program incorrect and sometimes they do it correct.

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