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.7 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM,FREEMAIL_REPLYTO,REPLYTO_WITHOUT_TO_CC autolearn=no
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,7a8ed246b4a23044
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.204.15.209 with SMTP id l17mr1044251bka.6.1345394004343;
        Sun, 19 Aug 2012 09:33:24 -0700 (PDT)
Received: by 10.236.191.33 with SMTP id f21mr7100992yhn.36.1345394003530;
        Sun, 19 Aug 2012 09:33:23 -0700 (PDT)
Path: 
 m12ni114323bkm.0!nntp.google.com!news1.google.com!u3no27590237qai.0!news-out.google.com!c6ni181615341qas.0!nntp.google.com!newsfeed2.dallas1.level3.net!news.level3.com!bloom-beacon.mit.edu!ra.nrl.navy.mil!nntp.club.cc.cmu.edu!news.unit0.net!feeds.phibee-telecom.net!dedekind.zen.co.uk!zen.net.uk!hamilton.zen.co.uk!reader01.nrc01.news.zen.net.uk.POSTED!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: Mechanisms for proving rules in .rlu files
Date: Sun, 19 Aug 2012 17:33:22 +0100
Message-ID: <MPG.2a9b257dd61575eb98969d@news.zen.co.uk>
References: <4365f56f-d4d3-440b-87bb-5cfe868608f5@googlegroups.com>
Reply-To: phil.jpthornley@gmail.com
MIME-Version: 1.0
User-Agent: MicroPlanet-Gravity/3.0.4
Organization: Zen Internet
NNTP-Posting-Host: 31d3c4d1.news.zen.co.uk
X-Trace: 
 DXC=Z;2_`3HhYV_R5C\68]hc6Wa0UP_O8AJo\=dR0\ckLKGPWeZ<[7LZNRVRQWS0lXYZ7\UhLi?]0KG=[0E^cgWZ>@\SkML7B7EO:hZ
X-Complaints-To: abuse@zen.co.uk
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2012-08-19T17:33:22+01:00
List-Id: <comp.lang.ada>

In article <4365f56f-d4d3-440b-87bb-5cfe868608f5@googlegroups.com>, 
benjaminhocking@gmail.com says...
> 
> I've created a fairly large .rlu file, and I'm newly aware of the "sparkrules" tool, but I haven't found a way to prove the validity of the rules in my .rlu file. For now, I've written a converter that converts the .rlu file to a PVS theory and I'm working on proving the rules there, but this converter makes a few assumptions that are valid for my rules (all variables are integers or booleans, I'm only using a 
may_be_replaced_by and may_be_deduced_from, etc.) and of course might have flaws in it that I haven't detected yet.
> 
> What mechanisms do others use for proving user-defined rules?
> 
> -Ben

I've always used the SPADE Proof Checker - because I was already using 
that when rules were first introduced, and it is trivial to create the 
corresponding VC from the rule as they are both written in FDL. A 
secondary consideration is that, if delivering the rules to a customer, 
they can also be given the proof scripts to repeat the validation 
themselves using only the SPARK tools.

On the assumptions about what types wildcards have, I reckon that it is 
safe to assume that the formulae generated by the Examiner are well 
formed, and that the code they are generated from is free of semantic 
errors.  So context restricts the possible types of the expression that 
will match to a wildcard.  I add checktype sideconditions as appropriate 
where there is any ambiguity.

... and on SPARKRules - have you considered whether it is necessary to 
validate its outputs?  Ie that the Simplifier rule files have been 
generated correctly.  This clearly has to be done independently of the 
process that generates these files and I included the reference for each 
rule in the generated file to allow a backwards check to the validated 
rule in the 'rule library'.

Cheers,

Phil