Re: Class wide preconditions: error in GNAT implementation?

["Randy Brukardt" <randy@rrsoftware.com>]

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