Spark_IO: improving with postconditions?

Spark_IO: improving with postconditions?

[Maciej Sobczak]

The Spark_IO package defines several procedures that "return" string
values by filling the given String object and the end-of-sequence
index value. This end-of-sequence parameter is consistently defined
as:

Stop : out Natural

One example of such a function is:

   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;

It would save the caller from one redundant check if the Stop value is
ever used again as index into the returned string value.

--
Maciej Sobczak * www.msobczak.com * www.inspirel.com

Database Access Library for Ada: www.inspirel.com/soci-ada

Re: Spark_IO: improving with postconditions?

[Georg Bauhaus]

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);

If so, another precodition might be needed, Item'Last in Natural;
If Get_Line (or for that matter, a program) can do useful
things with empty string buffers.  Is it desirable?

Re: Spark_IO: improving with postconditions?

[xavier grave]

-----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-----

Re: Spark_IO: improving with postconditions?

[Georg Bauhaus]

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.