Re: Trouble cutting loops with SPARK. Advice?

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

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