From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,ec6f74e58e86b38b X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news4.google.com!feeder1-2.proxad.net!proxad.net!feeder1-1.proxad.net!198.186.194.250.MISMATCH!news-xxxfer.readnews.com!news-out.readnews.com!postnews3.readnews.com!not-for-mail Message-Id: <4bfd998c$0$2359$4d3efbfe@news.sover.net> From: "Peter C. Chapin" Subject: Re: Lost in translation (with SPARK user rules) Newsgroups: comp.lang.ada Date: Wed, 26 May 2010 18:01:26 -0400 References: <0466e131-cc80-4db4-b080-eec9aefcb1c7@z17g2000vbd.googlegroups.com> <4bfd2d05$0$27598$ba4acef3@reader.news.orange.fr> <1jo6gjejsy828$.e9dx6txqbazd$.dlg@40tude.net> User-Agent: KNode/0.10.9 MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7Bit Organization: SoVerNet (sover.net) NNTP-Posting-Host: e0cfa8ac.news.sover.net X-Trace: DXC=];aR\[8=7gRRQfJ7=^R]EYK6_LM2JZB_SH\ERZ28IfFZ:WUUlR<856_L;TWA_637iTFh3M4en_TK_ X-Complaints-To: abuse@sover.net Xref: g2news2.google.com comp.lang.ada:12058 Date: 2010-05-26T18:01:26-04:00 List-Id: 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