Re: Trouble cutting loops with SPARK. Advice?

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 7 Mar, 11:20, Simon Wright <si...@pushface.org> wrote:
> Phil Thornley <phil.jpthorn...@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 ...

Well - he would have learned that it isn't valid SPARK :-)
(All initialization values must be static and slices aren't allowed
either)

Cheers,

Phil