Class wide preconditions: error in the Ada 2012 Rationale?

[Yannick Duchêne (Hibou57)]

I have a doubt, and this one disturb me, so this topic.

I was reading the revised version (fourth draft) of the Ada 2012
Rationale, when I saw this:

> However, the rules regarding preconditions are perhaps surprising.
> The specific precondition Pre for Equilateral_Triangle must be true
> (checked in the body) but so long as just one of the class wide
> preconditions Pre'Class for Object and Triangle is true then all iswell.

Then later, a summary of the rule:

> 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 statements are not compatible with the substitution 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?

There may be a comment on that point, see below, but first, an example
test, compiled with GNAT:


with Ada.Text_IO;

procedure Ex
is
package P1 is

type T is interface;
Condition : Boolean;

procedure P (E : T) is abstract
with Pre'Class => P1.Condition;
end;

package P2 is

type T is interface and P1.T;
Condition : Boolean;

overriding
procedure P (E : T) is abstract
with Pre'Class => P2.Condition;
end;

package P3 is

type T is new P2.T with null record;
Condition : Boolean;

overriding
procedure P (E : T)
with Pre'Class => P3.Condition;
end;

package body P3 is
procedure P (E : T)
is begin
Ada.Text_IO.Put_Line ("You're OK!");
end;
end;

E : P3.T;
begin
P1.Condition := True;
P2.Condition := True;
P3.Condition := True; -- Hint: try to set this to `False`.
E.P;
end Ex;


Side‑note: the package prefix added to access the condition in the
“Pre'Class”, are not strictly required, but required with GNAT to bypass
one of its bug.

Test this example modifying each of the conditions: it `P3.Condition` is
set to `False`, there won't be any error at runtime, and you'll be OK,
although `P3.Condition` is the specific precondition for the concrete
implementation. It will fails only if all preconditions are false. No
specific precondition seems to be checked in the body of `P`, or else it
would trigger an exception when `P3.Condition` is set to `False`.

GNAT's interpretation is compatible with my own, and does not seems to be
compatible with the one from the Rationale.

But there may be a trick? Let's try turning `E.P;` into `P3.P (E);`: same
result. Not let's try turning `P3.P (E);` into `P3.P (P3.T'(E));`: same
result. GNAT does not know about anything like specific precondition, and
I'm OK with GNAT this time.

So is this me not understanding the Rationale? Or the Rationale has either
wrong or unclear words?


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

[Yannick Duchêne (Hibou57)]

Le Mon, 05 Nov 2012 21:41:48 +0100, Yannick Duchêne (Hibou57)
<yannick...@yahoo.fr> a écrit:

> I have a doubt, and this one disturb me, so this topic.
>
> I was reading the revised version (fourth draft) of the Ada 2012
> Rationale, when I saw this:
>
>> However, the rules regarding preconditions are perhaps surprising.
>> The specific precondition Pre for Equilateral_Triangle must be true
>> (checked in the body) but so long as just one of the class wide
>> preconditions Pre'Class for Object and Triangle is true then all iswell.
>
> Then later, a summary of the rule:
>
>> 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.
>

Oh no! I forget the link:
http://www.ada-auth.org/standards/12rat/html/Rat12-2-3.html

Pardon me.

[sbelm...@gmail.com]

On Monday, November 5, 2012 3:41:57 PM UTC-5, Hibou57 (Yannick Duchêne) wrote:
>
> I believe either my understanding is wrong, or the Rationale is wrong. The
>
> above statements are not compatible with the substitution 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?
>

A foundation of the LSP is that you should not be strengthening preconditions for derived types. After all, when you substitue a child for a parent, you cannot know anything about the child, which includes any additional preconditions that have been added. If classwide preconditions are checked at the point of the call, then it might dispatch to subprograms with preconditions that haven't even been written yet (that it clearly cannot check beforehand).

-sb

[Randy Brukardt]

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

[Yannick Duchêne (Hibou57)]

Le Fri, 09 Nov 2012 01:57:51 +0100, Randy Brukardt <ra...@rrsoftware.com>
a écrit:

> My rule of thumb is that in a given derivation chain, you should only use
> one or the other.

I fully agree, and was thinking of the same conclusion.

> (I wanted to make that a requirement, but that was shot down.)

How shot down? (if the question is not too much inquisitive)

[Randy Brukardt]

"Yannick Duch�ne (Hibou57)" <yannick...@yahoo.fr> wrote in message

news:op.wnhfv7yjule2fv@cardamome...

Le Fri, 09 Nov 2012 01:57:51 +0100, Randy Brukardt <ra...@rrsoftware.com>

a �crit:

>> (I wanted to make that a requirement, but that was shot down.)
>How shot down? (if the question is not too much inquisitive)

I don't recall the details, but I think most people wanted as few
restrictions as possible. "Methodological restrictions" have a bad history
in Ada, and thus we often avoid them. Clearly a tool like AdaControl can
enforce style rules beyond those the language requires, and that was thought
to be the best option here.

Randy.