Re: Issue with SPARK 2014

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

On Wednesday, 14 October 2015 21:04:52 UTC+1, Stuart  wrote:
> On Tuesday, 13 October 2015 18:37:08 UTC+1, Serge Robyns  wrote:
> > I'm trying to use SPARK on a little game, so far only one error remains and I've no clue on how to fix this.  I've been trying various approaches.
> > Here is the code snippet (hopefully complete enough).
> ...
> > medium: loop invariant might fail after first iteration, requires Count1 <= Columns'pred - 1
> > medium: loop invariant might fail after first iteration, requires Count2 < Number_Of_Columns
> 
> It has been a while (and a few versions of SPARK) since I played with this, but I think the problem is that your loop invariants are not strong enough - they don't carry enough information around the loop.
> 
> IIRC the loop invariant acts as a cut point, and it is only information in the invariant that is carried around the loop, earlier knowledge derived from the modelling of the code and the pre-conditions is lost (unless it is embedded in the loop invariant).
> 
> In your first case the only knowledge carried around the loop is that:
>    Count1 was <= Integer (Columns'Pred (Column) - Columns'First)
>    and you incremented it.
> 
> Consequently, at the next iteration SPARK warns you that the Invariant might fail, because if it was equal to  Integer (Columns'Pred (Column) - Columns'First) before, it will now (because of the increment) be greater!!
> 
> Unfortunately I do not have access to a copy of SPARK or the manuals here to help you resolve it (I expect an expert will be along in a while), but I would guess that you need to strengthen the invariant to an equality statement that remains true.

Stuart's explanation is quite correct.

In the first version try changing the bound on Count1 to:
   Integer (Columns'Pred (Column) - J)
so that it starts at 0 and increments by 1 on each loop.

(and next time put up compilable code).

Cheers,

Phil