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!news1.google.com!npeer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nx02.iad01.newshosting.com!newshosting.com!198.186.194.249.MISMATCH!transit3.readnews.com!news-out.readnews.com!postnews3.readnews.com!not-for-mail Message-Id: <4bffaed5$0$2378$4d3efbfe@news.sover.net> From: "Peter C. Chapin" Subject: SPARK and testing. Was: Lost in translation (with SPARK user rules) Newsgroups: comp.lang.ada Date: Fri, 28 May 2010 07:57:46 -0400 References: <0466e131-cc80-4db4-b080-eec9aefcb1c7@z17g2000vbd.googlegroups.com> <4bfd2d05$0$27598$ba4acef3@reader.news.orange.fr> <1jo6gjejsy828$.e9dx6txqbazd$.dlg@40tude.net> <4bfd998c$0$2359$4d3efbfe@news.sover.net> <4bfebb3f$0$27571$ba4acef3@reader.news.orange.fr> 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: f75bcc9f.news.sover.net X-Trace: DXC=2ZIBI:2472of0OR[ak:C_fK6_LM2JZB_c=Pfm5Z7jCNa:WUUlR<856oN=F`OLc0Fmkm81mBF3N;Zg X-Complaints-To: abuse@sover.net Xref: g2news2.google.com comp.lang.ada:12120 Date: 2010-05-28T07:57:46-04:00 List-Id: Pascal Obry wrote: > Just curious, why do you feel that you still need to write tests after > having run successfully the SPARK proof checker? Despite the proofs testing is still essential. At least that is my view. Here is why: 1. The proofs show that the subprograms obey the annotations that I provide. However, there is nothing that I'm doing that formally links those annotations to the actual intended purpose of my code. My code might be correctly implemented (proved) but perhaps it correctly implements the wrong thing. I realize there are formal methods that address this issue, but I'm not using them. 2. The proofs only show that the source code is, in some sense, correct. However, they say nothing about the correctness of the code generated by the compiler or about how that code will interact with the operating system or hardware. Testing isn't as exhaustive as proof but it is a "top to bottom" method of checking one's code. If a test succeeds, the entire execution stack worked properly... for that case at least. My code tends to interact with hardware in a very low level way. What if I misunderstood what I read in the hardware data sheets? SPARK can't help me with that misunderstanding. 3. Some of what I want to test are "non-functional" requirements such as execution speed and memory consumption. There are also some usability issues to consider. It seems like these things are outside SPARK's domain. 4. I might get lazy or run out of time and not complete all the proofs. After a while testing becomes the easier path. I could believe that the rate of bug elimination per unit of development time might improve by switching over to testing before every single VC has been discharged. Of course this will depend on how experienced one is with the tools (and with testing), so I'm not sure if this is really true or not. In summary I've concluded that no matter how nifty it is to prove one's code using a tool like SPARK, testing remains a necessary step in the production of quality software. SPARK is great but it has a limited scope of applicability; there are important things that SPARK has nothing to say about. So I write test programs. Recently a collague of mine pointed me to the following article about recent radiation therapy machine accidents: http://www.nytimes.com/2010/01/24/health/24radiation.html?pagewanted=all He commented that SPARK might have helped to avoid those accidents. Based on my understanding of the article, I agree that SPARK might have been helpful to a degree. However, some of the problems that occurred were really related to poor user interface decisions and poor hospital procedures. I don't see how SPARK could have helped with that. However, appropriate user testing might have caught some of the problems. It seems to me that SPARK is all about building a correct *implementation*, but it says nothing about the correctness of the design. Peter