"Yannick Duch�ne (Hibou57)" <
yannick...@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.