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,322fd62c9ac2f5cc,start
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!q33g2000pra.googlegroups.com!not-for-mail
From: phil thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: ANN: Tokeneer - Proofs updated to use User Rules
Date: Mon, 27 Apr 2009 02:59:57 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <ebe82045-62c5-43bb-b52d-54a7f49cb691@q33g2000pra.googlegroups.com>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Trace: posting.google.com 1240826397 15420 127.0.0.1 (27 Apr 2009 09:59:57
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Mon, 27 Apr 2009 09:59:57 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: q33g2000pra.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.9)
	Gecko/2009040821 Firefox/3.0.9,gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:5550
Date: 2009-04-27T02:59:57-07:00
List-Id: <comp.lang.ada>

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