comp.lang.ada
 help / color / mirror / Atom feed
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.


  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