Lost in translation (with SPARK user rules)
in [ADA]
|
From: Phil Thornley on 27 May 2010 07:41 On 27 May, 12:32, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: [...] > Ok, found. I was not correct with the way to require the type to be > integer as done in > > my_set(1): (X=0) or (X=1) may_be_deduced_from [ integer(X), X>=0, X<=1 > ]. > > It has to be > > my_set(1): (X=0) or (X=1) may_be_deduced_from [ > goal(checktype(X,integer)), X>=0, X<=1 ]. > > I've check that > > my_set(1): (X=0) or (X=1) may_be_deduced_from [ goal(integer(X)), X>=0, > X<=1 ]. > > does not work, which lead to another question : what is the difference > between the two predicates integer(X) and checktype(X,integer) ? The > documentation is not clear to me about it. About checktype(EXPRESSION, > TYPE_IDENTIFIER), it says This predicate may be used to check that an > expression is of an appropriate type and about integer(EXPRESSION) is > says This built-in Prolog predicate succeeds if and only if its argument > is instantiated to an integer. So what's the difference between > goal(integer(X)) and goal(checktype(X,integer)). Does the latter > refers to root type as defined in source and the other to something else ? > (so what?) It's explained in the Simplifier manual section 7.2.3: goal(integer(X)) requires X to *be* an integer, not just of integer type (so goal(integer(42)) succeeds). If you always use goal(checktype(X, integer)) then is works for anything that has an integer type. > > Another strange thing is that the file NUMINEQS.RUL does not contains any > predicate stating arguments have to be integers and there is just a > comment in heading, nothing in rules about it. This is the documentation of a Checker rule file, so is not relevant to the Simplifier. In the actual rule file used by the Checker the comment that you mention will be included in what the Checker sees, so will be effective in restricting the application of the rule. Cheers, Phil
From: Phil Thornley on 27 May 2010 07:57 On 27 May, 13:22, stefan-lu...(a)see-the.signature wrote: [..] > Wouldn't it be much simpler to use the proof checker, instead of the > simplifier? The main reason that I have for avoiding the Proof Checker for VCs left after simplfication is that the proofs need to be repeated every time the VCs are generated - which is OK except that small and irrelevant changes to the code often break the proof scripts that you have to keep to do the reproofs each time. (And the Proof Checker provides no support for the maintenance of existing scripts.) So my approach is now to create user rules so that the Simplfier proves 100% of the VCs. However this sometimes requires quite complex user rules that are difficult validate manually, so I use the Proof Checker to validate those rules by creating VCs that correspond to the rule and proving those. There are a couple of small examples of this in the Tokeneer code distributed with SPARK GPL 8.1.1 - see code/core/tismain.rlu and code/ core/tismain/mainloopbody.rlu. Cheers, Phil
From: Mark Lorenzen on 27 May 2010 08:32 On 27 Maj, 00:01, "Peter C. Chapin" <pcc482...(a)gmail.com> wrote: > > Next I was able to prove the code free of runtime errors. This worked out > quite easily in this case. After changing two declarations to use properly > constrainted subtypes (rather than just Natural as I had originally... my > bad), the SPARK simplifier was able to discharge 96% of the VCs "out of the > box." The remaining ones were not hard to fix. I felt lucky! > > Now I hope to encode some useful and interesting information about the > intended functionality of the subprograms in SPARK annotations (#pre, #post, > etc), and see if I can still get the proofs to go through. Somewhere around > now I will also start building my test program. One thing that I like about > SPARK is that you can do a lot of useful things with it without worrying > about stubbing out a zillion supporting packages for purposes of creating a > test program. I would like to suggest that you always use the mandatory annotations (of course) *and also* the #pre annotation. The use of preconditions can drastically improve the Simplifier's ability to discharge VCs. You already discovered that effect when you introduced constrained subtypes. Furthermore you don't have to think about ways to make your subprograms total by using "nil" values or error flags, which also relieves the calling subprogram from checking for such "nil" values and error flags. Then, if you are bold, you can start to think about writing postconditions. *However*, if the criticality of your program *requires* the use of postconditions, I suggest that you introduce them from the beginning on as their introduction they may require some reworking (often simplification) of your code. - Mark L
From: Yannick Duchêne (Hibou57) on 27 May 2010 08:36 Le Thu, 27 May 2010 13:57:58 +0200, Phil Thornley <phil.jpthornley(a)googlemail.com> a écrit: > So my approach is now to create user rules so that the Simplfier > proves 100% of the VCs. However this sometimes requires quite complex > user rules that are difficult validate manually, so I use the Proof > Checker to validate those rules by creating VCs that correspond to the > rule and proving those. This is close to my personal wish too, except I see a slight difference : I prefer to write very simple user rules, easily proved (like as easy to prove as using a truth table) and write Check based demonstrations relying on these rules. This is because I feel it is more safe (enforce soundness) and because it left more in the source in less in external documents (does not brake source navigability and layout logic). -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise.
From: Yannick Duchêne (Hibou57) on 27 May 2010 08:42
Le Thu, 27 May 2010 13:41:08 +0200, Phil Thornley <phil.jpthornley(a)googlemail.com> a écrit: > It's explained in the Simplifier manual section 7.2.3: > goal(integer(X)) requires X to *be* an integer, not just of integer > type (so goal(integer(42)) succeeds). Thanks for the reference (may be I tend to become lazy when I am facing scattered documentations, oops) -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise. |