From: "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>
Subject: Class wide preconditions: error in the Ada 2012 Rationale?
Date: Mon, 05 Nov 2012 21:41:48 +0100
Date: 2012-11-05T21:41:48+01:00 [thread overview]
Message-ID: <op.wnbifyvyule2fv@cardamome> (raw)
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
next reply other threads:[~2012-11-08 5:40 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-11-05 20:41 Yannick Duchêne (Hibou57) [this message]
2012-11-05 20:43 ` Class wide preconditions: error in the Ada 2012 Rationale? Yannick Duchêne (Hibou57)
2012-11-06 1:04 ` sbelmont700
2012-11-09 0:57 ` Randy Brukardt
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