Re: Trouble cutting loops with SPARK. Advice?

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

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