From: xorquewasp@googlemail.com
Subject: Re: SPARK postcondition check fails
Date: Tue, 9 Jun 2009 00:12:43 -0700 (PDT)
Date: 2009-06-09T00:12:43-07:00 [thread overview]
Message-ID: <70bfaee3-59b7-486c-abff-4ca6b233598e@g20g2000vba.googlegroups.com> (raw)
In-Reply-To: 5a1a9746-2893-4c2e-a1b7-6107d33f2524@c19g2000yqc.googlegroups.com
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.
next prev parent reply other threads:[~2009-06-09 7:12 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 [this message]
2009-06-09 7:49 ` roderick.chapman
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox