From: xavier grave <xavier.grave@ipno.in2p3.fr>
Subject: Re: Spark_IO: improving with postconditions?
Date: Wed, 26 Aug 2009 16:47:44 +0200
Date: 2009-08-26T16:47:44+02:00 [thread overview]
Message-ID: <h73hug$vmg$1@ccpntc8.in2p3.fr> (raw)
In-Reply-To: <4a94ff1d$0$31876$9b4e6d93@newsspool3.arcor-online.net>
-----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-----
next prev parent reply other threads:[~2009-08-26 14:47 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-08-26 8:57 Spark_IO: improving with postconditions? Maciej Sobczak
2009-08-26 9:23 ` Georg Bauhaus
2009-08-26 14:47 ` xavier grave [this message]
2009-08-26 15:47 ` Georg Bauhaus
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox