From: roderick.chapman@googlemail.com
Subject: Re: SPARK postcondition check fails
Date: Mon, 8 Jun 2009 23:45:14 -0700 (PDT)
Date: 2009-06-08T23:45:14-07:00 [thread overview]
Message-ID: <5a1a9746-2893-4c2e-a1b7-6107d33f2524@c19g2000yqc.googlegroups.com> (raw)
In-Reply-To: 02cc303d-6a22-4f09-b174-d2fbbb422645@t10g2000vbg.googlegroups.com
> 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
next prev parent reply other threads:[~2009-06-09 6:45 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 [this message]
2009-06-09 7:12 ` xorquewasp
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