* Class Wide Type Invariants - My bug or compiler bug
@ 2014-02-26 3:29 Anh Vo
2014-02-26 22:35 ` adambeneschan
0 siblings, 1 reply; 5+ messages in thread
From: Anh Vo @ 2014-02-26 3:29 UTC (permalink / raw)
GNAT did not raise Assertion_Error where I thought it should for the following codes. Either I misunderstood the LRM or it is a compiler bug.
-- places.ads
package Places is
type Disc_Pt is tagged private
with Type_Invariant'Class => Check_In (Disc_Pt);
Initial_Disc_Pt : constant Disc_Pt;
function Check_In (D : Disc_Pt) return Boolean with Inline;
procedure Set_X_Coord (D : in out Disc_Pt; X : Float)
with Pre => (X >= -1.0 and then X <= 1.0);
procedure Set_Y_Coord (D : in out Disc_Pt; Y : Float)
with Pre => (Y >= -1.0 and then Y <= 1.0);
private
type Disc_Pt is tagged
record
X, Y : Float range -1.0 .. +1.0;
end record;
Initial_Disc_Pt : constant Disc_Pt := (others => 0.5);
end Places;
-- places.adb
package body Places is
function Check_In (D : Disc_Pt) return Boolean is
begin
return (D.X**2 + D.Y**2 <= 1.0);
end Check_In;
procedure Set_X_Coord (D : in out Disc_Pt; X : Float) is
begin
D.X := X;
end Set_X_Coord;
procedure Set_Y_Coord (D : in out Disc_Pt; Y : Float) is
begin
D.Y := Y;
end Set_Y_Coord;
end Places;
-- places.inner.ads
package Places.Inner is
type Ring_Pt is new Disc_Pt with private
with Type_Invariant'Class => Check_Out(Ring_Pt);
Initial_Ring_Pt : constant Ring_Pt;
function Check_Out (R : Ring_Pt) return Boolean
with Inline;
private
type Ring_Pt is new Disc_Pt with null record;
Initial_Ring_Pt : constant Ring_Pt := Ring_Pt'(Initial_Disc_Pt with null record);
function Check_Out (R : Ring_Pt) return Boolean is
(R.X**2 + R.Y**2 >= 0.25);
end Places.Inner;
-- invariants_inheritance_test.adb
with Ada.Text_Io;
with Ada.Exceptions; use Ada;
with Places.Inner;
procedure Invariants_Inheritance_Test is
use Text_Io;
Child_Pt : Places.Inner.Ring_Pt := Places.Inner.Initial_Ring_Pt;
begin
Places.Inner.Set_X_Coord(Child_Pt, 0.0); -- OK since 0.5**2 + 0.0 >= 0.25
Places.Inner.Set_Y_Coord(Child_Pt, 0.1); -- should fail Check_Out(...),
-- 0.1**2 + 0.0 < 0.25
exception
when Err : others =>
Put_Line ("Houston help!!! " & Exceptions.Exception_Information(Err));
end Invariants_Inheritance_Test;
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Class Wide Type Invariants - My bug or compiler bug
2014-02-26 3:29 Class Wide Type Invariants - My bug or compiler bug Anh Vo
@ 2014-02-26 22:35 ` adambeneschan
2014-02-26 23:59 ` Anh Vo
2014-02-27 1:01 ` Randy Brukardt
0 siblings, 2 replies; 5+ messages in thread
From: adambeneschan @ 2014-02-26 22:35 UTC (permalink / raw)
On Tuesday, February 25, 2014 7:29:45 PM UTC-8, Anh Vo wrote:
> GNAT did not raise Assertion_Error where I thought it should for the following codes. Either I misunderstood the LRM or it is a compiler bug.
It looks to me like this should work, according to 7.3.2(19). I don't know what GNAT's default Assertion_Policy for Type_Invariant'Class is, however.
-- Adam
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Class Wide Type Invariants - My bug or compiler bug
2014-02-26 22:35 ` adambeneschan
@ 2014-02-26 23:59 ` Anh Vo
2014-02-27 1:01 ` Randy Brukardt
1 sibling, 0 replies; 5+ messages in thread
From: Anh Vo @ 2014-02-26 23:59 UTC (permalink / raw)
On Wednesday, February 26, 2014 2:35:52 PM UTC-8, adambe...@gmail.com wrote:
> On Tuesday, February 25, 2014 7:29:45 PM UTC-8, Anh Vo wrote:
>
>> GNAT did not raise Assertion_Error where I thought it should for the following codes. Either I misunderstood the LRM or it is a compiler bug.
>
> It looks to me like this should work, according to 7.3.2(19). I don't know what GNAT's default Assertion_Policy for Type_Invariant'Class is, however.
GNAT did comply with 7.3.2(18/3) however.
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Class Wide Type Invariants - My bug or compiler bug
2014-02-26 22:35 ` adambeneschan
2014-02-26 23:59 ` Anh Vo
@ 2014-02-27 1:01 ` Randy Brukardt
2014-02-27 1:16 ` adambeneschan
1 sibling, 1 reply; 5+ messages in thread
From: Randy Brukardt @ 2014-02-27 1:01 UTC (permalink / raw)
<adambeneschan@gmail.com> wrote in message
news:3cf20663-960d-4ab1-9210-08042ca6af43@googlegroups.com...
> On Tuesday, February 25, 2014 7:29:45 PM UTC-8, Anh Vo wrote:
>> GNAT did not raise Assertion_Error where I thought it should for the
>> following codes. Either I misunderstood the LRM or it is a compiler bug.
>
> It looks to me like this should work, according to 7.3.2(19). I don't
> know what GNAT's
> default Assertion_Policy for Type_Invariant'Class is, however.
7.3.2(19/3) is a mess, however. AI12-0042-1 changed it a lot, but that
change isn't right either, so it's rather in limbo at the moment. (See the
working RM for the current state of things.)
Note that a literal implementation of 7.3.2(19/3) would cause every
invariant check to go infinitely recursive, since there is supposed to be an
invariant check on the parameter of Check_In, which is called from the
invariant check - repeat forever. GNAT doesn't implement that for obvious
reasons, so it can't exactly implement the rule as written, and once you
have to go off the grid, all bets are off.
Some parts will be in every rule (checking of in out and out parameters, for
instance), so you probably can assume those are checked. But that's about
it. Probably it would be better to not depend too much on Type_Invariants
until we figure out what rules actually make sense (and we find a set that
isn't insane for one reason or another).
Randy.
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Class Wide Type Invariants - My bug or compiler bug
2014-02-27 1:01 ` Randy Brukardt
@ 2014-02-27 1:16 ` adambeneschan
0 siblings, 0 replies; 5+ messages in thread
From: adambeneschan @ 2014-02-27 1:16 UTC (permalink / raw)
On Wednesday, February 26, 2014 5:01:45 PM UTC-8, Randy Brukardt wrote:
> 7.3.2(19/3) is a mess, however. AI12-0042-1 changed it a lot, but that
> change isn't right either, so it's rather in limbo at the moment. (See the
> working RM for the current state of things.)
>
> Note that a literal implementation of 7.3.2(19/3) would cause every
> invariant check to go infinitely recursive, since there is supposed to be an
> invariant check on the parameter of Check_In, which is called from the
> invariant check - repeat forever. GNAT doesn't implement that for obvious
> reasons, so it can't exactly implement the rule as written, and once you
> have to go off the grid, all bets are off.
>
> Some parts will be in every rule (checking of in out and out parameters, for
> instance), so you probably can assume those are checked. But that's about
> it. Probably it would be better to not depend too much on Type_Invariants
> until we figure out what rules actually make sense (and we find a set that
> isn't insane for one reason or another).
Interesting ... thanks.
-- Adam
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2014-02-27 1:16 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-02-26 3:29 Class Wide Type Invariants - My bug or compiler bug Anh Vo
2014-02-26 22:35 ` adambeneschan
2014-02-26 23:59 ` Anh Vo
2014-02-27 1:01 ` Randy Brukardt
2014-02-27 1:16 ` adambeneschan
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox