"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message 
news:op.wnbifyvyule2fv@cardamome...
>I have a doubt, and this one disturb me, so this topic.
>
...
>> In summary, class wide preconditions are checked at the point of call. 
>> Class wide postconditions and both specific pre- and postconditionsare 
>> checked in the actual body.
>
>I believe either my understanding is wrong, or the Rationale is wrong.

The above is correct.

> The above statements are not compatible with the substitution principle.

*Specific* preconditions and postconditions are not necessarily compatible 
with the substitution principle. If you want that, you either have to be 
careful what you write, or (better IMHO) use only class-wide preconditions 
and postconditions.

You don't always want strict LSP, and using specific preconditions gives you 
a way to get that when needed. But of course, in that case, dispatching 
calls may fail for no reason visible at the point of the call. (LSP = Liskov 
Substitutability Principle).

> What if a sub-program expects a a class wide type with a root type and its 
> precondition, and get a derived type with a specific precondition it can't 
> know about?

You still evaluate the specific precondition associated with the subprogram 
that is actually called.

My understanding is that a lot of GNAT users only use carefully written 
specific preconditions (probably because they learned how to do that before 
class-wide preconditions existed in GNAT). Those can be, but don't have to, 
follow LSP. OTOH, class-wide preconditions follow LSP by design.

My rule of thumb is that in a given derivation chain, you should only use 
one or the other. (I wanted to make that a requirement, but that was shot 
down.)

I think given the sorts of programs that you write, you should only use 
class-wide preconditions and postconditions, and forget that specific ones 
exist at all. In which case, you won't have a problem with LSP.

                                       Randy.