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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,4876056933faf283
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!news3.google.com!proxad.net!feeder1-2.proxad.net!194.25.134.126.MISMATCH!newsfeed01.sul.t-online.de!t-online.de!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Wed, 26 Aug 2009 17:47:26 +0200
From: Georg Bauhaus <rm.tsoh.plus-bug.bauhaus@maps.futureapps.de>
Reply-To: rm.tsoh+bauhaus@maps.futureapps.de
User-Agent: Thunderbird 2.0.0.23 (Windows/20090812)
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Spark_IO: improving with postconditions?
References: <a6cc46c0-eab3-4a77-b3dd-ee870d85c936@18g2000yqa.googlegroups.com>
 <4a94ff1d$0$31876$9b4e6d93@newsspool3.arcor-online.net>
 <h73hug$vmg$1@ccpntc8.in2p3.fr>
In-Reply-To: <h73hug$vmg$1@ccpntc8.in2p3.fr>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
Message-ID: <4a955910$0$30227$9b4e6d93@newsspool1.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 26 Aug 2009 17:47:28 CEST
NNTP-Posting-Host: 960fdfe2.newsspool1.arcor-online.net
X-Trace: 
 DXC=HO0S6E`KS20]E=H1Q9`787ic==]BZ:af>4Fo<]lROoR1^YC2XCjHcb9QMh\\V]IH02A:ho7QcPOV3cI9=DH<bgI3]MMdfK9c3j2
X-Complaints-To: usenet-abuse@arcor.de
Xref: g2news2.google.com comp.lang.ada:7998
Date: 2009-08-26T17:47:28+02:00
List-Id: <comp.lang.ada>

xavier grave wrote:
> Georg Bauhaus a �crit :
>> Maciej Sobczak schrieb:
> 
>>>    procedure Get_Line (File     : in     File_Type;
>>>                        Item     :    out String;
>>>                        Stop     :    out Natural);
>>>    --# global in out Inputs;
>>>    --# derives Inputs,
>>>    --#         Item,
>>>    --#         Stop     from Inputs, File;
>>>    --# declare delay;
>>>
>>> Wouldn't it be good to enhance this specification with additional:
>>>
>>>    --# post Stop <= Item'Last;
>> Will Spark accept this String?
> 
>>    X : String (-1 .. -2);
> 
> In Ada the String declaration is the following :
> type String is array(Positive range <>) of Character;
> 
> So I think Spark wouldn't accept your String declaration.

7p6 doesn't, and the messages refer to two different
things.  (It is all logical, I had already forgotten
this nice property of SPARK.)  Say,

   subtype Null_Range is Positive range 1 .. 0;
   subtype XString is String(Null_Range);
   X : XString;

A null range is not accepted (It is, in Ada).
String types must have a lower bound of 1 (by rule 3.6.3)
So range -1 .. -2, which again is valid Ada,
is of anonymous type in SPARK, and hence not valid.
It's just that the second message is confusing without
the first


   5     subtype Null_Range is Positive range 1 .. 0;
                                              ^
***        Semantic Error    :409: Empty range specified.

   6     subtype XString is String(Null_Range);
                                   ^
***        Semantic Error    :417: String subtypes must have a lower
index bound of
           1.

My initial comment is really meaningless.