From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,7875892b95c5219d
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!postnews.google.com!b7g2000pre.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: ANN: Tokeneer - Proofs updated to use User Rules
Date: Thu, 30 Apr 2009 04:10:43 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <01abc18a-f849-4de7-82a5-c9752893d926@b7g2000pre.googlegroups.com>
References: ebe82045-62c5-43bb-b52d-54a7f49cb691@q33g2000pra.googlegroups.com
	<1286a815-8cfc-4ed2-97c6-ece7ec7c8923@w35g2000prg.googlegroups.com>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1241089843 19596 127.0.0.1 (30 Apr 2009 11:10:43
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 30 Apr 2009 11:10:43 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: b7g2000pre.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB;
 rv:1.9.0.10)
	Gecko/2009042316 Firefox/3.0.10,gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:5621
Date: 2009-04-30T04:10:43-07:00
List-Id: <comp.lang.ada>

On Apr 29, 8:20=A0am, roderick.chap...@googlemail.com wrote:
> On Apr 27, 10:59=A0am, 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. =A0We'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.

> =A0What 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