Lost in translation (with SPARK user rules)
in [ADA]
|
From: Maciej Sobczak on 28 May 2010 05:39 On 27 Maj, 20:34, Pascal Obry <pas...(a)obry.net> wrote: > Just curious, why do you feel that you still need to write tests after > having run successfully the SPARK proof checker? Because the SPARK proof checker does not guarantee the lack of infinite loops in the program? -- Maciej Sobczak
From: Yannick Duchêne (Hibou57) on 29 May 2010 19:03 Le Wed, 26 May 2010 12:09:17 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > Lost in translation... do you know the movie ? > No, I'm joking, this is not about this 2002 movie, that's about SPARK, > and exactly, > about translating some expressions in the rules language. > [...] In this area, the Simplifier sometimes shows slight capacities to be boring. Let a Check clause be â--# check ((2 ** Count) < (2 ** 8)) -> (Count < 8);â Let a user rule be âmy_rule: ((X ** Y) < (X ** Z)) -> (Y < Z) may_be_deduced_from [some-obvious-conditions].â There should be an exact match, isn't it ? Well, I guess you guess: it fails to prove the Check clause. Now, if you would like to know why, here is: it replaces this by â2 ** count < 256 -> count < 8â, ... it turns â(2 ** 8)â into â256â, so that it can't see any more an exact match with the user rule I've check in the *.SLG file, this is indeed due to simplification, this is not due to an hypothetical related error. -- 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 30 May 2010 02:55 Le Sun, 30 May 2010 01:03:31 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > Let a Check clause be â--# check ((2 ** Count) < (2 ** 8)) -> (Count < > 8);â > Let a user rule be âmy_rule: ((X ** Y) < (X ** Z)) -> (Y < Z) > may_be_deduced_from [some-obvious-conditions].â > > There should be an exact match, isn't it ? > > Well, I guess you guess: it fails to prove the Check clause. Now, if you > would like to know why, here is: it replaces this by â2 ** count < 256 > -> count < 8â, ... it turns â(2 ** 8)â into â256â, so that it can't see > any more an exact match with the user rule I didn't wanted to add rules for all constants, like 256, and etc. Fortunately, there is a somewhat cleaner way to work around, which still involves a constant, but a nice one : 2. If âmy_rule(1): ((X ** Y) < (X ** Z)) -> (Y < Z) may_be_deduced_from [...].â is completed with another rule like, âmy_rule(2): ((2 ** Y) < (2 ** Z)) -> (Y < Z) may_be_deduced_from [...].â, then it did not change anymore 2 ** 8 into 256 and see a match. I don't know what it do in the background, nor why it preserve the expression when the rule to match contains at least a constant, however, what is nice with this work around, it that it will work with all powers of two. I still would like to know about the details : why when X is replaced by the literal 2, it does not match the same way ? Important to notice anyway. -- 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: Phil Thornley on 30 May 2010 05:26 On 30 May, 00:03, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > In this area, the Simplifier sometimes shows slight capacities to be > boring. > > Let a Check clause be --# check ((2 ** Count) < (2 ** 8)) -> (Count < 8); > Let a user rule be my_rule: ((X ** Y) < (X ** Z)) -> (Y < Z) > may_be_deduced_from [some-obvious-conditions]. > > There should be an exact match, isn't it ? > > Well, I guess you guess: it fails to prove the Check clause. Now, if you > would like to know why, here is: it replaces this by 2 ** count < 256 -> > count < 8, ... it turns (2 ** 8) into 256, so that it can't see any > more an exact match with the user rule > > I've check in the *.SLG file, this is indeed due to simplification, this > is not due to an hypothetical related error. The full description of all the simplification steps is in section 3 of the Simplifier User Manual, so if you read this and follow through the steps in a simplification log file then you should get a better understanding of how the tool works - and so how to write user rules that are effective. Application of user rules is the final step (out of about a dozen) that the Simplifier uses, so at that point a conclusion is likely to have been changed from the form of the annotation that generated it. In the case you describe here Count must be defined as a constant with value 8, and that replacement is the first step that the Simplifier takes. Then it will convert 2**8 to 256 in a subsequent step. (A basic strategy of the Simplifier is to replace any expressions with a simpler version wherever possible - perhaps that's why it called the Simplifier rather than the 'Prover' :-). Section 3.12 describes how the Simplifier uses user rules - and it is clear from this description that the rule needs to match expressions in the VC as they are at the end of the process, not as in the original VC. You can see why this is sensible (even if it has some drawbacks*). Generally the way that a user rule is written is in response to an unproven conclusion in a simplified VC, so the author of the rule uses the final form of the unproven VC to write the rule. Therefore the rule can only be reliably applied at the point where the VC has reached its final form. I guess it might be possible for the Simplifier to try all the user rules at each stage of the process - but the developers of the tool have been concentrating heavily on making simplification as quick as possible (quite rightly in my view) and would not want to do anything that might slow it down without a very strong argument for the advantages of doing that. * The main drawback that I see is that some user rules define replacements that must be made for the VC to be provable, but at present these are made too late for them to be effective, since the Simplifier has already exhausted all its other strategies. It would be nice to have replacements defined in user rules applied in the first simplification stage, how about: my_rewrite(1): A must_be_replaced_by B if [...] . (Of course nothing is ever simple, for example what happens if one rewrite rule requires another to be applied before its sideconditions are satisfied - are all such rules tried repeatedly until none are used, or is it a once-only pass? etc...) Cheers, Phil
From: Phil Thornley on 30 May 2010 05:30
On 30 May, 07:55, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: [...] > I still would like to know about the details : why when X is replaced by > the literal 2, it does not match the same way ? I would guess that the Simplifier manages to match 2**Y to 256 (by instantiating Y with 8), but not X**Y. Cheers, Phil |