Re: SPARK

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

Le Sun, 16 May 2010 07:28:16 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:

> Request for confirmation.
>
> In Praxis's documentations, there is a file named Checker_Rules.pdf,  
> title is “SPADE Proof Checker Rules Manual”, which list Checker's  
> built-in rules. I do not see any reason why the Examiner/Simplifier  
> would have a different rules set than the Checker, so I suppose this  
> rules set is also the one used by the Examiner/Simplifier. I would just  
> want to be sure : someone can confirm ?
>
> If it is, this may explain why I meet some troubles proving one thing  
> with real arithmetic (yes, I know real arithmetic is not safe and I must  
> care, but this is just an exercise...)

About adding rules.

The Praxis document named Checker_Rules.pdf says

> The tool Buildchlib is no longer shipped with the Checker
> following the release of version 2.05. The use of
> user-defined rule files is still permitted, through the
> consult command. For further information contact
> Praxis High Integrity Systems.
So there is no way to add a rule system-wide as I was expecting.

Attempting to change the content of an *.RUL file in the lib/checker/rules  
directory, has no effect at all. The rules seems really compiled inside  
Simplifier and Checker.

Here are the rules I was to add in NUMINEQS.RUL:

    inequals(122):  X/Y<1     may_be_deduced_from [ X>=0, Y>0, Y>X ].
    inequals(123):  X/Y<1     may_be_deduced_from [ X<=0, Y<0, Y<X ].
    inequals(124):  X/Y>(-1)  may_be_deduced_from [ X>=0, Y<0, (-Y)>X ].
    inequals(125):  X/Y>(-1)  may_be_deduced_from [ X<=0, Y>0, Y>(-X) ].

It works only if added in an .RLU file.

Note: writing something like ...

    inequals(124):  X/Y>(-1)  may_be_deduced_from [ X>=0, Y<0,  
abs(Y)>abs(X) ].

... although parsed correctly, will turns into a rule which may not be  
applied by Simplifier. It seems rules must be given in the most  
straightforward way. This may explain why ARITH.RUL contains such a thing:

    arith(1):    X*1             may_be_replaced_by X.
    arith(2):    1*X             may_be_replaced_by X.

Commutativity seems not expected to be automatically applied or attempted.

About the rules I was to add, I tried something like:

    inequals(122):  [ X/Y>=0, X/Y<1 ]    may_be_deduced_from [ X>=0, Y>0,  
Y>X ].

This is at least parsed without syntax error message, but not applied.

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.


Have a nice day



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

Wanted: if you know about some though in the area of comparisons between  
SPARK and VDM, please, let me know. Will enjoy to talk with you about it.