Re: Lost in translation (with SPARK user rules)

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Wed, 26 May 2010 12:38:52 +0200, Phil Thornley  
<phil.jpthornley@googlemail.com> a écrit:
> I don't think there us anything wrong with these rules, but the
> Simplifier will not use a *combination* of user rules to discharge a
> proof.  (They are not as 'powerful' as the built-in rules as they are
> not consulted until the Simplifier has tried all its other
> strategies).
>
> For example, section 7.3.1 of the Simplifier User Manual says:
>    "For an inference rule of the form
>       rulename(1): Goal may_be_deduced_from Conditions.
>    the Simplifier will attempt to find a means of instantiating
>    all of the wildcards in Goal such that it becomes an exact
>    match for an existing undischarged conclusion."
>
> This means that a single inference rule is applied only if it
> *directly* matches a conclusion.
>
> Also, since user rules are applied right at the end, you have to use
> the form of the conclusion as it appears in the SIV file, so:
>> One entertaining thing: I've noticed “and 1” is always replaced by “mod  
>> 2” in the simplifier's *.SIV output files. As an example, the latter  
>> Check  clause is replaced by:
>>
>>     C1:    bit__and(instance, 2) = 0 -> instance div 2 mod 2 = 0 .
>
> If that is the conclusion left in the SIV file then the user rule to
> prove it is:
>    user_bitwise(1): bit__and(X, 2) = 0 -> X div 2 mod 2 = 0
> may_be_deduced .
I remember about this, this was just that I did not suspected this had to  
be a so exact match.

> (and a minor comment is that it is probably not a good idea to use the
> Proof Checker rule family names for Simplifier user rules - it just
> adds to the confusion about how the rules are used.)
Oops, sorry, I though this was better to go on with an existing naming  
convention already established.


Overall so far to me.

I don't know what to think about one feeling, may be I'm wrong: I feel a  
bit discouraged with SPARK now. I wonder if this is really this thing I  
was waiting for so long (I am referring to some of my previous words about  
it in another thread).

May be I should give up with it.

If I could believe they could be some funding or a market for that, I  
would like to work on another system in this area... but I don't think so  
(I don't think there are many people expecting this kind of things).

Well, for the time being, I feel I gonna forget about it at least for some  
time and go on without it.

-- 
There is even better than a pragma Assert: a SPARK --# check.