ANN: Tokeneer - Proofs updated to use User Rules

ANN: Tokeneer - Proofs updated to use User Rules

[phil thornley]

The Tokeneer code is an excellent example of SPARK, but the work was
completed several years ago and prior to major improvements being made
to the proof capabilities of the SPARK Toolset.  Consequently the
published example does not fully demonstrate those capabilities nor
does it provide examples of how to use them.

I have now revised many of the proofs to use User Rules, with a
reduction in unsimplified VCs from 110 to 24. The Proof Checker is not
now required to complete any of the proofs (although it is still used
to prove VCs that justify two of the rules).

The files needed to update the published version of Tokeneer are
available from www.sparksure.com. There is a note included with the
files describing the changes made and the approach used.

Phil Thornley

Re: ANN: Tokeneer - Proofs updated to use User Rules

[roderick.chapman]

On Apr 27, 10:59 am, phil thornley <phil.jpthorn...@googlemail.com>
wrote:
> I have now revised many of the proofs to use User Rules, with a
> reduction in unsimplified VCs from 110 to 24.

Nice work Phil.  We're planning to release an updated
Tokeneer package later this year following the GPL release
of the SPARK Toolset, so we'll try to include these
if that's OK.  What licence are your new rules under?
 - Rod, SPARK Team

Re: ANN: Tokeneer - Proofs updated to use User Rules

[Phil Thornley]

On Apr 29, 8:20 am, roderick.chap...@googlemail.com wrote:
> On Apr 27, 10:59 am, phil thornley <phil.jpthorn...@googlemail.com>
> wrote:
>
> > I have now revised many of the proofs to use User Rules, with a
> > reduction in unsimplified VCs from 110 to 24.
>
> Nice work Phil.  We're planning to release an updated
> Tokeneer package later this year following the GPL release
> of the SPARK Toolset, so we'll try to include these
> if that's OK.

I'll be more than happy for you to include them in an updated Tokeneer
release.

>  What licence are your new rules under?

The files are supplied for anyone to use as they want, with no
restricitions on how they can be used. I'll sort out actual terms for
your copies by email.

Phil Thornley