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,ec6f74e58e86b38b
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!a20g2000vbc.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: Lost in translation (with SPARK user rules)
Date: Thu, 27 May 2010 04:57:58 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <ecb1930e-58eb-47e3-9a5f-c6eb12793fe0@a20g2000vbc.googlegroups.com>
References: <op.vda45rsfule2fv@garhos>
 <0466e131-cc80-4db4-b080-eec9aefcb1c7@z17g2000vbd.googlegroups.com>
	<op.vda7dlc2ule2fv@garhos> <op.vdcuhhymule2fv@garhos>
 <op.vdc1x3ctule2fv@garhos>
	<Pine.LNX.4.64.1005271420410.30605@medsec1.medien.uni-weimar.de>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
X-Trace: posting.google.com 1274961478 9533 127.0.0.1 (27 May 2010 11:57:58
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 27 May 2010 11:57:58 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: a20g2000vbc.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
	Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
	3.0.30729; Media Center PC 6.0),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:12077
Date: 2010-05-27T04:57:58-07:00
List-Id: <comp.lang.ada>

On 27 May, 13:22, stefan-lu...@see-the.signature wrote:
[..]
> Wouldn't it be much simpler to use the proof checker, instead of the
> simplifier?

The main reason that I have for avoiding the Proof Checker for VCs
left after simplfication is that the proofs need to be repeated every
time the VCs are generated - which is OK except that small and
irrelevant changes to the code often break the proof scripts that you
have to keep to do the reproofs each time.
(And the Proof Checker provides no support for the maintenance of
existing scripts.)

So my approach is now to create user rules so that the Simplfier
proves 100% of the VCs.  However this sometimes requires quite complex
user rules that are difficult validate manually, so I use the Proof
Checker to validate those rules by creating VCs that correspond to the
rule and proving those.

There are a couple of small examples of this in the Tokeneer code
distributed with SPARK GPL 8.1.1 - see code/core/tismain.rlu and code/
core/tismain/mainloopbody.rlu.

Cheers,

Phil