SPARK and testing. Was: Lost in translation (with SPARK user rules)

["Peter C. Chapin" <pcc482719@gmail.com>]

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