From: Phil Thornley <phil.jpthornley@gmail.com>
Subject: Re: Mechanisms for proving rules in .rlu files
Date: Sun, 19 Aug 2012 17:33:22 +0100
Date: 2012-08-19T17:33:22+01:00 [thread overview]
Message-ID: <MPG.2a9b257dd61575eb98969d@news.zen.co.uk> (raw)
In-Reply-To: 4365f56f-d4d3-440b-87bb-5cfe868608f5@googlegroups.com
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
prev parent reply other threads:[~2012-08-19 16:33 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-08-17 20:39 Mechanisms for proving rules in .rlu files Ben Hocking
2012-08-17 21:37 ` Alexander Senier
2012-08-19 16:33 ` Phil Thornley [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox