Trouble cutting loops with SPARK. Advice?

["Peter C. Chapin" <pcc482719@gmail.com>]

I'm attempting to use SPARK to prove a simple function is free of run time
errors. Here is the (simplified) package specification:

package Strings is

   Max_Line_Length : constant := 225;
   subtype Line_Index is Positive range 1 .. Max_Line_Length;
   subtype Line_Size_Type is Natural range 0 .. Max_Line_Length;
   subtype Line_Type is String(Line_Index);
   type Line_Record is
      record
         Text : Line_Type;
         Size : Line_Size_Type;
      end record;

   function Prepare_Line(Line : String) return Line_Record;

end Strings;

This package provides a type Line_Record that holds a variable length string
in a fixed size buffer. As you can see the lines are limited to 225
characters. The function Prepare_Line copies the given string into a
Line_Record and returns it. If the string is too long it is truncated.

Okay... here is the implementation:

package body Strings is

   function Prepare_Line(Line : String) return Line_Record is
      Result : Line_Record;
      Characters_To_Copy : Line_Size_Type;
   begin
      Result.Text := Line_Type'(others => ' ');
      if Line'Length > Max_Line_Length then
         Characters_To_Copy := Max_Line_Length;
      else
         Characters_To_Copy := Line'Length;
      end if;
      for I in Line_Size_Type range 1 .. Characters_To_Copy loop
         Result.Text(I) := Line(Line'First + (I - 1));
      end loop;
      Result.Size := Characters_To_Copy;
      return Result;
   end Prepare_Line;

end Strings;

The problem is with the loop that actually copies the characters from the
provided String into the Line_Record. SPARK generates a verification
condition that it can't prove related to the "run time check" on the line in
the body of the loop. The SPARK Examiner warns about using a default
assertion to cut the loop. I understand that I should probably provide my own
assertion. My problem is that I can't quite figure out what I need to say.

If I write an assertion in the loop that involves the loop index variable, I,
the generated verification conditions appear to try to prove that the
assertion holds even for one extra iteration. That is, there is a VC that
tries to prove that if the assertion is true, then it must be true for the
next iteration. However that does not need to be so on the last iteration
(since there is no next iteration in that case) so the condition can't be
proved.

Specifically I get conclusions like "I <= 224." That can't be proved because,
in fact, sometimes I = 225 (the last time through the loop in the case where
the source String is being truncated).

Okay... but if I stay away from talking about I in the assertion, what can I
assert that will help convince SPARK that the array access operations are
fine? I've tried a few things... I can be more specific if necessary. So far,
no joy.

I get the feeling there is a trick here that I'm overlooking. Is my code
wrong? It looks okay to me. :)

Peter