Mechanisms for proving rules in .rlu files

Mechanisms for proving rules in .rlu files

[Ben Hocking]

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

Re: Mechanisms for proving rules in .rlu files

[Alexander Senier]

On Fri, 17 Aug 2012 13:39:47 -0700 (PDT)
Ben Hocking <benjaminhocking@gmail.com> wrote:

> What mechanisms do others use for proving user-defined rules?

We do not prove user-defined rules, but work on the SIV (or VCG) files
directly, using the HOL-SPARK verification environment [1] of Isabelle.

Regards
Alex

[1]
http://isabelle.in.tum.de/library/HOL/HOL-Word/HOL-SPARK/Manual/document.pdf

Re: Mechanisms for proving rules in .rlu files

[Phil Thornley]

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