From: Serge Robyns <serge.robyns@gmail.com>
Subject: Re: Issue with SPARK 2014
Date: Mon, 19 Oct 2015 02:13:19 -0700 (PDT)
Date: 2015-10-19T02:13:19-07:00 [thread overview]
Message-ID: <6001b84e-41a0-4092-bc43-b00f4522d94a@googlegroups.com> (raw)
In-Reply-To: <mvvm5v$1oth$1@adenine.netfront.net>
>
> The messages that you get without an explicit loop invariant are because the
> default loop invariant isn't strong enough for this code.
What is missing to make this one stronger? Looks like missing a point.
> I don't think that you need more than one Loop_Variant in any loop, this is
> only needed to prove termination of the loop and just one valid loop variant
> should be enough.
>
OK, I capture the the point of the variants part. Looks like wanted to be too verbose.
Regards,
Serge
prev parent reply other threads:[~2015-10-19 9:13 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
2015-10-15 17:28 ` Serge Robyns
2015-10-18 8:44 ` Phil Thornley
2015-10-19 9:13 ` Serge Robyns [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox