From: roderick.chapman@googlemail.com
Subject: Re: SPARK postcondition check fails
Date: Tue, 9 Jun 2009 00:49:45 -0700 (PDT)
Date: 2009-06-09T00:49:45-07:00 [thread overview]
Message-ID: <2b6870e7-0846-4b52-932a-34ab3a86b946@g19g2000yql.googlegroups.com> (raw)
In-Reply-To: 70bfaee3-59b7-486c-abff-4ca6b233598e@g20g2000vba.googlegroups.com
On Jun 9, 8:12 am, xorquew...@googlemail.com wrote:
> On Jun 9, 7:45 am, roderick.chap...@googlemail.com wrote:
>
> > > You'll have to forgive the possibly naive question, there's quite
> > > a learning curve.
>
> > Habe you run the Simplifier over the generated VCs?
>
> > The Examiner _generates_ the VCs, but you need to run "sparksimp"
> > to Simplify them, then "pogs" to collate the results. Please see
> > chapter 10 of the SPARK book, or the Tokeneer Discovery tutorial
> > for more details.
> > - Rod Chapman
>
> No, I hadn't.
>
> I actually wasn't aware of the existence of the Tokeneer tutorial.
> I'll be going through that ASAP.
>
> By the SPARK book, do you mean High Integrity Ada by John Barnes?
>
> Thanks.
It's High Integrity _Software_ - the one with the blue cover
published in 2003 (but now in its 4th re-print...) Get it
from amazon.co.uk.
- Rod
prev parent reply other threads:[~2009-06-09 7:49 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-06-09 4:55 SPARK postcondition check fails xorquewasp
2009-06-09 6:45 ` roderick.chapman
2009-06-09 7:12 ` xorquewasp
2009-06-09 7:49 ` roderick.chapman [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