Class Wide Type Invariants - My bug or compiler bug

Class Wide Type Invariants - My bug or compiler bug

[Anh Vo]

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;

Re: Class Wide Type Invariants - My bug or compiler bug

[adambeneschan]

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

Re: Class Wide Type Invariants - My bug or compiler bug

[Anh Vo]

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.

Re: Class Wide Type Invariants - My bug or compiler bug

[Randy Brukardt]

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

Re: Class Wide Type Invariants - My bug or compiler bug

[adambeneschan]

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