From: Stuart <google_news@palin-26.freeserve.co.uk>
Subject: Re: Issue with SPARK 2014
Date: Wed, 14 Oct 2015 13:04:50 -0700 (PDT)
Date: 2015-10-14T13:04:50-07:00 [thread overview]
Message-ID: <4187f92b-770a-4d76-85c0-14f2eba2dee8@googlegroups.com> (raw)
In-Reply-To: <c4a5963b-78eb-4b55-83f5-a1de6b10717d@googlegroups.com>
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.
next prev parent reply other threads:[~2015-10-14 20:04 UTC|newest]
Thread overview: 11+ messages / expand[flat|nested] mbox.gz Atom feed top
2015-10-13 17:37 Issue with SPARK 2014 Serge Robyns
2015-10-13 20:40 ` joakimds
2015-10-14 15:25 ` Serge Robyns
2015-10-14 6:16 ` Simon Wright
2015-10-14 15:23 ` Serge Robyns
2015-10-14 20:04 ` Stuart [this message]
2015-10-15 8:44 ` Phil Thornley
2015-10-15 11:23 ` Stuart
2015-10-15 17:28 ` Serge Robyns
2015-10-18 8:44 ` Phil Thornley
2015-10-19 9:13 ` Serge Robyns
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox