From: "Randy Brukardt" <randy@rrsoftware.com>
Subject: Re: Class wide preconditions: error in the Ada 2012 Rationale?
Date: Thu, 8 Nov 2012 18:57:51 -0600
Date: 2012-11-08T18:57:51-06:00 [thread overview]
Message-ID: <k7hkeh$kuu$1@munin.nbi.dk> (raw)
In-Reply-To: op.wnbifyvyule2fv@cardamome
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2025 bytes --]
"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.
next prev parent reply other threads:[~2012-11-16 8:53 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-11-05 20:41 Class wide preconditions: error in the Ada 2012 Rationale? Yannick Duchêne (Hibou57)
2012-11-05 20:43 ` Yannick Duchêne (Hibou57)
2012-11-06 1:04 ` sbelmont700
2012-11-09 0:57 ` Randy Brukardt [this message]
2012-11-09 1:32 ` Yannick Duchêne (Hibou57)
2012-11-09 2:13 ` Randy Brukardt
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox