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-Thread: 103376,8d7393f07c06c5e9
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!news2.google.com!npeer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!news-in-02.newsfeed.easynews.com!easynews.com!easynews!transit4.readnews.com!news-out.readnews.com!postnews3.readnews.com!not-for-mail
Date: Sun, 29 Aug 2010 10:20:47 -0400
From: "Peter C. Chapin" <chapinp@acm.org>
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 6.1; en-US;
 rv:1.9.2.8) Gecko/20100802 Lightning/1.0b2 Thunderbird/3.1.2
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Another question about fixed point types.
References: <4c7991c8$0$2375$4d3efbfe@news.sover.net>
 <62f49eaf-ed47-47c7-a13a-96ca5750b4e8@y11g2000yqm.googlegroups.com>
 <4c7a44d1$0$2390$4d3efbfe@news.sover.net>
 <fe942a67-b3f8-4195-bf7e-6e10201cb715@i13g2000yqe.googlegroups.com>
In-Reply-To: 
 <fe942a67-b3f8-4195-bf7e-6e10201cb715@i13g2000yqe.googlegroups.com>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Message-ID: <4c7a6d04$0$2390$4d3efbfe@news.sover.net>
Organization: SoVerNet (sover.net)
NNTP-Posting-Host: a93f7576.news.sover.net
X-Trace: 
 DXC=FM=NKl<7`3BP7I;=`^Ef6@K6_LM2JZB_ClXHJXGi>>6I:WUUlR<856O;B3njnU2l9LHCAbKT=<mnG
X-Complaints-To: abuse@sover.net
Xref: g2news1.google.com comp.lang.ada:13809
Date: 2010-08-29T10:20:47-04:00
List-Id: <comp.lang.ada>

On 2010-08-29 08:31, Phil Thornley wrote:

> I was referring to the SPARK annotation that tells the Examiner which
> predefined type the compiler will use as the base type of a type
> declaration - it's needed for overflow checks and looks like:
> 
>    type An_Int is range -10_000 .. 10_000;
>    --# assert An_Int'Base is Short_Integer;
> 
> where the range for Short_Integer is defined in the SPARK
> configuration file

I see, okay. So am I right in saying that one should provide one of
these annotations for every scalar type definition in a SPARK program?
I'm guessing that by doing so SPARK could prove more automatically since
it would have more information. On the other hand it then becomes my
responsibility to get the base type right.

Peter