From: Phil Thornley <phil.jpthornley@googlemail.com>
Subject: Re: Trouble cutting loops with SPARK. Advice?
Date: Sun, 7 Mar 2010 03:41:55 -0800 (PST)
Date: 2010-03-07T03:41:55-08:00 [thread overview]
Message-ID: <7b98c325-ce1d-4882-bbae-cfd816f29749@b7g2000yqd.googlegroups.com> (raw)
In-Reply-To: 4b938750$0$2334$4d3efbfe@news.sover.net
> Great! Thanks for the help. That does make things a bit clearer. The assertion
> you showed works for me as well, but I'll try to take away a more general
> lesson from this. I'm in the process of proving a more complete program free
> of runtime errors and so far I've got about 1/2 of it done. However, I'm
> pretty sure the situation I described here comes up several times in the
> remaining code (with variations, of course).
Peter
Glad that worked - I'm always happy to help with SPARK problems
(particularly proof ones). If you wany any help by email (perhaps
because the code is too big for a news message) use my address on
www.sparksure.com.
Cheers,
Phil
next prev parent reply other threads:[~2010-03-07 11:41 UTC|newest]
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-03-06 20:33 Trouble cutting loops with SPARK. Advice? Peter C. Chapin
2010-03-07 10:22 ` Phil Thornley
2010-03-07 11:04 ` Peter C. Chapin
2010-03-07 11:41 ` Phil Thornley [this message]
2010-03-07 11:20 ` Simon Wright
2010-03-07 11:43 ` Phil Thornley
2010-03-07 16:27 ` Simon Wright
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox