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: a07f3367d7,4876056933faf283
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!news3.google.com!feeder.news-service.com!de-l.enfer-du-nord.net!usenet-fr.net!proxad.net!feeder1-2.proxad.net!news.in2p3.fr!in2p3.fr!not-for-mail
From: xavier grave <xavier.grave@ipno.in2p3.fr>
Newsgroups: comp.lang.ada
Subject: Re: Spark_IO: improving with postconditions?
Date: Wed, 26 Aug 2009 16:47:44 +0200
Organization: In2p3
Message-ID: <h73hug$vmg$1@ccpntc8.in2p3.fr>
References: <a6cc46c0-eab3-4a77-b3dd-ee870d85c936@18g2000yqa.googlegroups.com>
 <4a94ff1d$0$31876$9b4e6d93@newsspool3.arcor-online.net>
NNTP-Posting-Host: ipnnarval.in2p3.fr
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: ccpntc8.in2p3.fr 1251298064 32464 134.158.92.7 (26 Aug 2009 14:47:44
 GMT)
X-Complaints-To: newsmaster@cc.in2p3.fr
NNTP-Posting-Date: Wed, 26 Aug 2009 14:47:44 +0000 (UTC)
User-Agent: Mozilla-Thunderbird 2.0.0.19 (X11/20090103)
In-Reply-To: <4a94ff1d$0$31876$9b4e6d93@newsspool3.arcor-online.net>
X-Enigmail-Version: 0.95.0
Xref: g2news2.google.com comp.lang.ada:7996
Date: 2009-08-26T16:47:44+02:00
List-Id: <comp.lang.ada>

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

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.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkqVSxAACgkQVIZi0A5BZF5RYwCeNsyk06Gs8NePyq8rrG4EC81W
dfIAnAsEAkODXWQjCLbvt90q7TTRsiFZ
=FTnE
-----END PGP SIGNATURE-----