Re: Class wide preconditions: error in GNAT implementation?

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

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