Trouble cutting loops with SPARK. Advice?

Trouble cutting loops with SPARK. Advice?

[Peter C. Chapin]

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

Re: Trouble cutting loops with SPARK. Advice?

[Phil Thornley]

Peter,

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

Your code is OK and yes there is something that you are probably
overlooking.

It's not really a 'trick' - more an oddity of the language for proving
code in 'for' loops that have range constraints.  (Loops like that are
the one exception to the SPARK rule that there are no anonymous
subtypes.)

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.  The Examiner doesn't check to see whether
Characters_To_Copy is changed within the loop (it just assumes that it
might be changed), so in this case you have to state that it is
unchanged in the loop assertion.

SPARK therefore supplies a notation for the value of any variable on
entry to a loop - append % to the name - so Characters_To_Copy% within
a proof context in the loop means the value of Characters_To_Copy on
entry to the loop.

The loop assertion that works for the code in your message is:
         --# assert I >= 1
         --#  and   Characters_To_Copy <= Line'Length
         --#  and   Characters_To_Copy = Characters_To_Copy%;
placed at the beginning of the loop.

Cheers,

Phil

Re: Trouble cutting loops with SPARK. Advice?

[Peter C. Chapin]

Phil Thornley wrote:

> 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.  The Examiner doesn't check to see whether
> Characters_To_Copy is changed within the loop (it just assumes that it
> might be changed), so in this case you have to state that it is
> unchanged in the loop assertion.

Great! Thanks for the help. That does make things a bit clearer. The assertion
you showed works for me as well, but I'll try to take away a more general
lesson from this. I'm in the process of proving a more complete program free
of runtime errors and so far I've got about 1/2 of it done. However, I'm
pretty sure the situation I described here comes up several times in the
remaining code (with variations, of course).

Thanks again.

Peter

Re: Trouble cutting loops with SPARK. Advice?

[Simon Wright]

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 ...

Re: Trouble cutting loops with SPARK. Advice?

[Phil Thornley]

> Great! Thanks for the help. That does make things a bit clearer. The assertion
> you showed works for me as well, but I'll try to take away a more general
> lesson from this. I'm in the process of proving a more complete program free
> of runtime errors and so far I've got about 1/2 of it done. However, I'm
> pretty sure the situation I described here comes up several times in the
> remaining code (with variations, of course).

Peter

Glad that worked - I'm always happy to help with SPARK problems
(particularly proof ones). If you wany any help by email (perhaps
because the code is too big for a news message) use my address on
www.sparksure.com.

Cheers,

Phil

Re: Trouble cutting loops with SPARK. Advice?

[Phil Thornley]

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

Re: Trouble cutting loops with SPARK. Advice?

[Simon Wright]

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

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

Hmpf. Much better Ada, though (IMO, of course).