Lost in translation (with SPARK user rules)
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 26 May 2010 17:14 Le Wed, 26 May 2010 22:14:48 +0200, Dmitry A. Kazakov <mailbox(a)dmitry-kazakov.de> a écrit: > No run time checks, but an option to tell more about the contract, with > enforced static checks, that this indeed hold. If you have no time, no > guts, or when the algorithm does not allow certain proofs, you just do > not > make promises you cannot keep and go further. OK, I see : you mean interfacing between Ada and SPARK ? Is that the idea ? Indeed, would be nice if Ada compiler could fee SPARK Examiner with required condition (provided I've understood your words). > I think it should be more than just two levels. But yes, each language > construct and each library operation shall have a contract. Goes the same way as the above (OK) >> Actually, how can you test an compiler >> compliance with SPARK ? I feel you can do it only for full Ada. > > Likely yes, because there exist legal Ada programs, such that no Ada > compiler could compile. So this could be one added good reason to have a test suit targeting the SPARK subset only. > Rather by refining the contracts. When you feel that the implementation > is > mature, you can add more promises to the contract of and see if they hold > (=provable). If they don't you could try to re-implement some parts of > it. > When you feel that it takes too much time, is impossible to prove, you > can > drop the idea to do it formally. You will sill have a gain of deeper > understanding how the thing works and could document why do you think it > is > correct, even if that is not formally provable. This seems to mean something similar to one of my previous message, about the fact I was perhaps targeting too much at first sight. Having different levels in mind seems indeed a requirement if one don't want to be too much discouraged. -- There is even better than a pragma Assert: a SPARK --# check.
From: Yannick Duchêne (Hibou57) on 26 May 2010 17:15 Le Wed, 26 May 2010 23:14:24 +0200, Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> a écrit: > Indeed, would be nice if Ada compiler could fee SPARK Examiner with > required condition Typo error : read âIndeed, would be nice if Ada compilers could *feed* Examiner with required conditionsâ -- There is even better than a pragma Assert: a SPARK --# check.
From: Peter C. Chapin on 26 May 2010 18:01 Dmitry A. Kazakov wrote: > Rather by refining the contracts. When you feel that the implementation is > mature, you can add more promises to the contract of and see if they hold > (=provable). If they don't you could try to re-implement some parts of it. > When you feel that it takes too much time, is impossible to prove, you can > drop the idea to do it formally. You will sill have a gain of deeper > understanding how the thing works and could document why do you think it is > correct, even if that is not formally provable. I think this is a good way to work with SPARK. I'm developing a SPARK program now. I started with the specifications, working with them until I felt comfortable with the overall structure of the program. Refactoring at that stage was very cheap and I did it several times. I just finished coding the body of the one of the critical packages. The SPARK Examiner was very helpful at catching silly errors that I might have missed. In one case I forget to condition a flag at the end of a procedure and was told that my code did not agree with my annotations. Nice. 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 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. Peter
From: Peter C. Chapin on 26 May 2010 18:06 Pascal Obry wrote: > The fact that your are working on a boundary. The secure SPARK on one > side and the OS non-SPARK foreign world. One difficult part was that > this is IO (stream like) where data are read from the same socket but > two consecutive read won't return the same value. There is way in SPARK > to deal with that, to avoid SPARK complaining that you have ineffective > code... not straight forward! Is this the sort of thing external own variables are intended to handle? Peter
From: Peter C. Chapin on 26 May 2010 18:17
Yannick Duchêne (Hibou57) wrote: > That is where I was not agree with a previous similar sentence from > someone else. I don't see a reason why only critical applications should > benefit of verifiability. This would not be a waste to apply standard > logic to program construction, and I even feel this should be an expected > minimum. I think the reason is that it's hard. SPARK's restrictions exist, in part, to create a language that can manipulated in a reasonably formal way using current technology. As soon as you start adding back exceptions, dynamic memory, recursion, etc, etc, it becomes very hard (beyond the state of the art?) to say significant things statically in formal way. Yet those features *are* very useful for many programs. I know there has been a lot of work done in the field of static analysis and I hope the field continues to advance. As it does, SPARK, or something like it, may be able to take on some of the complicated features it currently avoids. Also, depending on your needs, other kinds of static analysis might be useful besides formally proving program properties. So what I'm saying is that it may be premature to think about incorporating the SPARK sublanguage formally into the Ada standard. SPARK is a tool... one of many. I look forward to even better tools in the future! For example take a look at this: http://www.adacore.com/home/products/codepeer/ I believe this tool works with full Ada and it sounds pretty neat. Disclaimer: I haven't tried it. Peter |