Lost in translation (with SPARK user rules)
in [ADA]
|
From: Phil Thornley on 27 May 2010 09:38 On 27 May, 13:36, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr> wrote: > Le Thu, 27 May 2010 13:57:58 +0200, Phil Thornley > <phil.jpthorn...(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). 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). Cheers, Phil
From: Pascal Obry on 27 May 2010 14:34 Peter, > I do agree certainly that SPARK is not for everything. The code I'm working on > is (potentially) security sensitive so the extra effort of working with SPARK > seems worthwhile. My test harness, on the other hand, is likely to be in full > Ada. Just curious, why do you feel that you still need to write tests after having run successfully the SPARK proof checker? Pascal. -- --|------------------------------------------------------ --| Pascal Obry Team-Ada Member --| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE --|------------------------------------------------------ --| http://www.obry.net - http://v2p.fr.eu.org --| "The best way to travel is by means of imagination" --| --| gpg --keyserver keys.gnupg.net --recv-key F949BD3B
From: Pascal Obry on 27 May 2010 14:39 Peter, > Is this the sort of thing external own variables are intended to handle? Yes, that's what I thought at first. But for some reasons (I don't remember now) this was not working in this case (sorry, I really have a bad memory!). I had designed 3 or 4 different spec and had help from the SPARK team before converging on a working one. Pascal. -- --|------------------------------------------------------ --| Pascal Obry Team-Ada Member --| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE --|------------------------------------------------------ --| http://www.obry.net - http://v2p.fr.eu.org --| "The best way to travel is by means of imagination" --| --| gpg --keyserver keys.gnupg.net --recv-key F949BD3B
From: Yannick Duchêne (Hibou57) on 27 May 2010 15:18 Le Thu, 27 May 2010 20:34:52 +0200, Pascal Obry <pascal(a)obry.net> a écrit: > Peter, > >> I do agree certainly that SPARK is not for everything. The code I'm >> working on >> is (potentially) security sensitive so the extra effort of working with >> SPARK >> seems worthwhile. My test harness, on the other hand, is likely to be >> in full >> Ada. > > Just curious, why do you feel that you still need to write tests after > having run successfully the SPARK proof checker? > > Pascal. Good question Pascal, May be because that's a tradition, may be because some inside voices tell you you're bad if you don't run test, or may be due to the lack of understanding that test are done when there is no way to prove anything (that is, tests would be a fall-back). Peter, I'm not telling that's you though, I'm just telling that testing is so much genetically inlaid in the computer culture, that doing without it, would be somewhat frightening, just like the first time one learn to swim or to ride a bicycle (waw, do I really have to stand up on this thing which not even able to stand up by itself ?) But may be there is another reason : logic. That is a question I have in mind since I've recently discovered (well, really started with) SPARK : one may prove something, while he/she may not really know what he/she is proving. You may prove some specifications (I mean pre/post, not runtime error safety), but what if this specifications does not express what he/she supposed these expressed ? One component of the chain may still be a source of matters : the one from a though to a specification. I agree testing is a least a bit needed for that. However, this is not to be driven as the other kind of testing, which is very different, I mean the one which is driven when nothing else can be done (or no body wanted to do something else). -- 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: Warren on 27 May 2010 15:53
=?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= expounded in news:op.vda45rsfule2fv(a)garhos: > 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. That movie sucked and was boring. I'm not joking. ;-) Warren |