Spark_IO: improving with postconditions?

[Maciej Sobczak <see.my.homepage@gmail.com>]

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