SPARK
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 18 May 2010 14:01 Le Sun, 16 May 2010 07:28:16 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)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..
From: Phil Thornley on 19 May 2010 04:09 On 18 May, 19:01, Yannick Duchêne (Hibou57) <yannick_duch...(a)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!
From: Simon Wright on 19 May 2010 16:38 Phil Thornley <phil.jpthornley(a)googlemail.com> writes: > * Except that, of course, the full source of the Simplifier is > available, and there is nothing to stop you making changes to it! I believe you need the non-free (ie, quite expensive) SICSTUS Prolog system to build the tools from source (there is SICSTUS-special code which doesn't work under GNU Prolog). The GPL SPARK 8.1.1 binary release doesn't run well under Mac OS X Snow Leopard (problems with exception handling in 64-bit executables).
From: Yannick Duchêne (Hibou57) on 19 May 2010 17:27 Le Wed, 19 May 2010 22:38:07 +0200, Simon Wright <simon(a)pushface.org> a écrit: > Phil Thornley <phil.jpthornley(a)googlemail.com> writes: > >> * Except that, of course, the full source of the Simplifier is >> available, and there is nothing to stop you making changes to it! > > I believe you need the non-free (ie, quite expensive) Question on side: Why is it always either free or either expansive ? Why not multiple levels between both of these extremities ? > SICSTUS Prolog > system to build the tools from source (there is SICSTUS-special code > which doesn't work under GNU Prolog). You may be true, as I remember an old topic (about two one years ago and a half), of someone getting into trouble trying to build SPARK with his favorite Prolog compiler. > The GPL SPARK 8.1.1 binary release doesn't run well under Mac OS X Snow > Leopard (problems with exception handling in 64-bit executables). Where does the SPARK executable makes use of exceptions ? I have read something asserting the SPARK system is it-self checked to be runtime exceptions free. Perhaps this is in an external dependency part.
From: Yannick Duchêne (Hibou57) on 19 May 2010 17:35
Le Wed, 19 May 2010 10:09:33 +0200, Phil Thornley <phil.jpthornley(a)googlemail.com> a écrit: > 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)" Thanks for the detail Phil. > * Except that, of course, the full source of the Simplifier is > available, and there is nothing to stop you making changes to it! Simon has tell about a limit in this area. I see another, which is the biggest to me : this would be a kind of forking, and a fork is not any more something common. This would be a valid way for my own use only, which could not be shared any more ; someone else could not check something from me using his/her own SPARK installation. I use to be interested is some specifications of some other languages of the like, which I've never found, and gave up with the idea (of the probably too much big work) to attempt to create one, for this exact reason : this would be specific to me, to what I use. In this area, it is mandatory to have standards, otherwise, this is not as much interesting. This is not only about checking for validity, this is also about expressing why it is so to others in way hey can trust and read. |