From: Stuart <google_news@palin-26.freeserve.co.uk>
Subject: Re: Issue with SPARK 2014
Date: Thu, 15 Oct 2015 04:23:39 -0700 (PDT)
Date: 2015-10-15T04:23:39-07:00 [thread overview]
Message-ID: <e904f96f-5913-4256-b827-5520767ee19c@googlegroups.com> (raw)
In-Reply-To: <41a7f7f9-65b4-43a3-b817-f5d9c6a3d015@googlegroups.com>
On Thursday, 15 October 2015 09:44:39 UTC+1, Phil Thornley wrote:
...
> Stuart's explanation is quite correct.
[Thank you :-)]
> 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.
...
Having thought about it a bit more (but still no opportunity to test) I thought that example 1 could use the invariant:
Count1 = Integer(J-Columns'First)
This seems to capture the essence of the loop (always a good sign for a loop invariant)
In the absence of the full code getting a definitive useful loop invariant is not possible!
next prev parent reply other threads:[~2015-10-15 11:23 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
2015-10-15 8:44 ` Phil Thornley
2015-10-15 11:23 ` Stuart [this message]
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