Re: Spark_IO: improving with postconditions?

[Georg Bauhaus <rm.tsoh.plus-bug.bauhaus@maps.futureapps.de>]

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.