Lost in translation (with SPARK user rules)
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 30 May 2010 05:46 Le Sun, 30 May 2010 11:30:29 +0200, Phil Thornley <phil.jpthornley(a)googlemail.com> a écrit: > > I would guess that the Simplifier manages to match 2**Y to 256 (by > instantiating Y with 8), but not X**Y. > > Cheers, > > Phil That would be a bit more than just matching so, this is a seed of solving. -- 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 05:57 Le Sun, 30 May 2010 11:26:12 +0200, Phil Thornley <phil.jpthornley(a)googlemail.com> a écrit: > 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. Yes, I know. The nut with me, is that I try to find the best way to use these rules as general rules, and precisely avoid to write rules which would only match expressions in a given unproved VC. The technique is evolving, it works better than at my very first attempts. May be I will write some french pages about it some day. > 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. I guess this is important, as I've notice the simplifier is easily slowed down as the number of checks increase (or may be this is the effect of my user rules, which I suppose, are not as much efficiently handled as the built-in ones). > (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...) That is why, except with one unique single case (a rewrite rule involving modular types), my own rule is to not use rewrite rules at all, because it can easily become a one way trap only. Inference rules are more plastic and does not stick anything. -- 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 1 Jun 2010 01:42 A little test I did right a few seconds ago. Let a rule be of the form: C1 may_be_deduced_from [C2, V]. Which is so that this one is valid too: C2 may_be_deduced_from [C1, V]. So finally, C1 and C2 and both either conclusion or condition. This may *logically* (not by pattern) match three other things: C1 -> C2 may_be_deduced_from [V]. C2 -> C1 may_be_deduced_from [V]. C1 <-> C2 may_be_deduced_from [V]. Although only one would be required, which is C1 <-> C2 may_be_deduced_from [V]. Instead one need to have (and write) all of: C1 may_be_deduced_from [C2, V]. C2 may_be_deduced_from [C1, V]. C1 -> C2 may_be_deduced_from [V]. C2 -> C1 may_be_deduced_from [V]. C1 <-> C2 may_be_deduced_from [V]. Five rules instead of one, where one logical rule would be sufficient. I wanted to get ride of this, with these generic rules, which I hoped will help and solve this recurrent trick: A may_be_deduced_from [B, B -> A]. A may_be_deduced_from [B, B <-> A]. B may_be_deduced_from [A, B <-> A]. B -> A may_be_deduced_from [B <-> A]. A -> B may_be_deduced_from [B <-> A]. I though this would ends to exact matches, and I would have only to write rules of the form C1 <-> C2 may_be_deduced_from [V]. ... <-> ... may_be_deduced_from [...]. or of the form C1 -> C2 may_be_deduced_from [V]. ... -> ... may_be_deduced_from [...]. and expected I would have to write only this, avoiding duplications of multiple equivalent forms (I expected these equivalent forms would be deduced via the above generic rules). Unfortunately, and although this looks like there should be exact matches after instantiations, this does not work (rules does not match in Simplifier). Now I really see why there is the restriction of user rules which are to be defined on package or subprogram basis (while I still don't enjoy this) : this test clearly demonstrate there is no way to write general rules, these are always specifics to a VC or a set of VC for a given package or subprogram. Or else, all logical equivalences need to be written explicitly (which in turn requires great care when one want to review rules, as duplication -- I know it after experiences -- does not help safety and help to miss weakness). Note: SPARK is still useful ;) with these words, I don't wanted to say it is not good -- 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 2 Jun 2010 22:44
Le Thu, 27 May 2010 15:38:27 +0200, Phil Thornley <phil.jpthornley(a)googlemail.com> a écrit: > I very much agree with this approach - adding a sequence of check > annotations so that the rules required are easy to validate. However > you have to balance this against the size of the annotations required. > > For example, a few years ago I was trying to prove the correctness of > code for a red-black tree, the single rotation procedure was four > lines of code, but it took about 60 lines of check annotations plus a > bunch of quite complex rules, to prove that the tree stayed a valid > binary tree (and I never got round to proving the colour invariants). At least, I've noticed that while user rules can have an impact on speed of Simplifier, this is not the most important. Check (and so assert also) seems to have the most significant impact. What is worth to note : a long and explicit proof does not implies it is a slower one (the Simplifier is mostly slow when it fails to prove something, and is faster when it success). -- 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. |