Re: Trouble cutting loops with SPARK. Advice?

[Simon Wright <simon@pushface.org>]

Phil Thornley <phil.jpthornley@googlemail.com> writes:

> The problem is that the value of the variables that provide the loop
> bounds (in your code the variable Characters_To_Copy) can be changed
> within the loop, so any reference to Characters_To_Copy within an
> assertion in the loop means the *current* value, not the value that
> defined the loop bound.

Would it have helped if Peter had said, instead of

      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;

this:

      Characters_To_Copy : constant Line_Size_Type
        := Line_Size_Type'Min (Line'Length, Max_Line_Length);
   begin
      Result.Text := Line_Type'(others => ' ');

And I'm sure one could eliminate the loop by proper slicing. Of course,
that would reduce the SPARK learning experience ...