From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,77f1de37204ed8a6
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2001-06-03 13:14:47 PST
Newsgroups: comp.lang.ada
Path: 
 archiver1.google.com!newsfeed.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!newsfeed.cwix.com!newsfeed.nyc.globix.net!uunet!ash.uu.net!world!bobduff
From: Robert A Duff <bobduff@world.std.com>
Subject: Re: Operator visibility question
Sender: bobduff@world.std.com (Robert A Duff)
Message-ID: <wccbso5fhj3.fsf@world.std.com>
Date: Sun, 3 Jun 2001 20:13:52 GMT
References: <ba18d5cb.0106030548.62aa45e2@posting.google.com>
Organization: The World Public Access UNIX, Brookline, MA
X-Newsreader: Gnus v5.3/Emacs 19.34
Xref: archiver1.google.com comp.lang.ada:8042
Date: 2001-06-03T20:13:52+00:00
List-Id: <comp.lang.ada>

rod@praxis-cs.co.uk (Rod Chapman) writes:

> Can anyone please tell me if the following code is legal?

In what language -- Ada or SPARK?  ;-) ;-)

> package MT
> is
>    type T is range 0 .. 4;
> end MT;
> 
> with MT;
> --# inherit MT;
> package VT
> is
>    function "+" (Left, Right : in MT.T) return MT.T renames MT."+";
>    A : constant := 2;
>    B : constant MT.T := 3;
> 
>    C : constant Boolean := (A + 2) < B; -- Is "<" visible here?

There are several "<" operators directly visible here, including the one
for root_integer.  But none of them apply -- the "<" for MT.T is not
directly visible here.  So I believe this is illegal in Ada, unless I'm
missing something.

A and 2 are both of type universal_integer, and there are implicit
conversions from u_i to any integer type, but there is no implicit
conversion from MT.T to root_real.

Sounds like a GNAT bug.  Seems like SPARK is correct here.

> end VT;
> 
> The SPARK Examiner rejects the declaration of C with the message:
> 
>    9     C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
>                                          ^
> ***        Semantic Error    :309: Operator not visible for these types.
> 
> On the other hand, GNAT 3.13 accepts the code with no errors.  Can anyone
> explain which is right, and (more importantly) why?
>  Cheers,
>   Rod Chapman
>   SPARK Team
>   Praxis Critical Systems