Re: SPARK

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 18 May, 19:01, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> I've noticed Simplifier seems to read an .RUL file it is belongs to a  
> directory where it is reading .VCG files (I don't why it do that). I've  
> noticed that while I was playing a bit with it :p
>
> Will have to search for another way to add rules system-wide, if possible.

Yannick,

I don't think that the toolset provides what you are looking for*.

The only recognised way to supply additional rules to the Simplifier
are as user rules - the full details about this are in Section 7 of
the Simplifier user manual.  This section also describes how the user
rules are applied.

It is unfortunate that user rules are less effective than the rules
built into the Simplifier as they are only used once the normal
Simplifier strategies have failed to prove a conclusion (see the
introduction of Section 3).

For example an inference rule will only be used if it *directly*
proves a conclusion.
Section 7.2.1: "In order for the Simplifier to be able to make use of
the rule, it must find an instance of the rule by pattern-matching it
against the current VC (for inference rules, this essentially means
against the undischarged conclusions of the VC)"

Cheers,

Phil

* Except that, of course, the full source of the Simplifier is
available, and there is nothing to stop you making changes to it!