Requesting critique of a C unit test environment

Ben Bacarisse said:

> Richard Heathfield <rjh@see.sig.invalid> writes:
>
>> Ben Bacarisse said:
>>
<snip>
>>>
>>> A machine assisted proof of
>>> the actual code could be expected to inspire a little more
>>> confidence.
>>
>> Why? Presumably the machine that is doing the assisting is itself a
>> computer program. What makes you think the assistance program is
>> correct?
>
> What do you test your software with if not more software?

A rolling pin. Any software that can withstand the pastry test is likely
to be able to withstand anything else too.

> If you think that a machine assisted proof would not inspire "a little
> more" confidence than a hand proof, then I won't try to persuade you
> (it was a modest enough claim)

Yes, on reflection I see that I'm guilty of (accidentally) extending
your claim, which was indeed modest enough.

<snip>

--
Richard Heathfield <http://www.cpax.org.uk>
Email: -www. +rjh@
Google users: <http://www.cpax.org.uk/prg/writings/googly.php>
"Usenet is a strange place" - dmr 29 July 1999

Ben Bacarisse <ben.usenet@bsb.me.uk> writes:

> Richard Heathfield <rjh@see.sig.invalid> writes:
>
>> Erik Wikström said:
>>> Testing is used to find errors, while formal methods are used to prove
>>> that there are no errors, at least that's the goal. So if you can
>>> prove that there are no errors why test for them?
>>
>> "Beware of bugs in the above code; I have only proved it correct, not
>> tried it." - Donald E Knuth.
>
> But this was a "by hand" proof in 1977. A machine assisted proof of
> the actual code could be expected to inspire a little more confidence.

YMMV of course, but if I could get Donald Knuth to prove my
programs correct "by hand", I'd feel no need for additional
confidence.
--
Ben Pfaff
http://benpfaff.org

Flash Gordon wrote:

> You have missed out internal formal testing which in many environments
> is far more complete than acceptance testing. For example, I've worked
> on projects where a formal test literally takes a week to complete but
> the customer acceptance testing takes only a few hours.

What did y'all do if the "formal" test failed?

What I look for is this: Replicate the failure as a short unit test. Not a
proof - just a stupid test that fails because the code change needed to fix
that formal test isn't there.

The point is to make the fast tests higher value as you go...

--
Phlip
http://www.oreilly.com/catalog/9780596510657/

Ben Pfaff <blp@cs.stanford.edu> writes:

> Ben Bacarisse <ben.usenet@bsb.me.uk> writes:
>
>> Richard Heathfield <rjh@see.sig.invalid> writes:
>>
>>> Erik Wikström said:
>>>> Testing is used to find errors, while formal methods are used to prove
>>>> that there are no errors, at least that's the goal. So if you can
>>>> prove that there are no errors why test for them?
>>>
>>> "Beware of bugs in the above code; I have only proved it correct, not
>>> tried it." - Donald E Knuth.
>>
>> But this was a "by hand" proof in 1977. A machine assisted proof of
>> the actual code could be expected to inspire a little more confidence.
>
> YMMV of course, but if I could get Donald Knuth to prove my
> programs correct "by hand", I'd feel no need for additional
> confidence.

No, MMIS[1]. I did not intend to disparage Prof. Knuth's "hand
proofs" (what a thought!) but rather to say that the problem he is
referring to is as likely to be that one proves something other than
the program one has written (or later writes) as it is to be that ones
proof is (internally) flawed.

I suspect that he is not entirely happy with the way that quip is used
so often to suggest the pointlessness of proofs[2] (after all, what
did he choose to do with his "Notes on van Emde Boas constriction of
priority deques" -- a proof rather than a test implementation!).

[1] "My mileage is similar".
[2] This not one of those times -- RH was just countering the much
stronger assertion that proof => no need to test.

--
Ben.

On Aug 27, 4:17 pm, Ben Bacarisse <ben.use...@bsb.me.uk> wrote:
[snip]
> I suspect that he is not entirely happy with the way that quip is used
> so often to suggest the pointlessness of proofs[2] (after all, what
> did he choose to do with his "Notes on van Emde Boas constriction of
> priority deques" -- a proof rather than a test implementation!).

Aside:
Working vEB tree implementation here:
http://www.itu.dk/people/kokholm/veb/

Flash Gordon wrote:
> Ian Collins wrote, On 27/08/07 21:51:
>> Flash Gordon wrote:
>>> Ian Collins wrote, On 27/08/07 08:14:
>>>> Ark Khasin wrote:
>>>>> Ian Collins wrote:
>>> <snip>
>>>
>>>>>>> And finally there is a port issue (it's an embedded type talking
>>>>>>> ). I
>>>>>>> am proposing something that requires only the compiler.
>>>>>>>
>>>>>> Shouldn't matter for unit testing, develop and test on a hosted
>>>>>> system.
>>>>>> If you require bits of the target environment, mock (simulate) them.
>>>>>>
>>>>> The farthest I can go away from the target is a software simulator of
>>>>> the instruction set. Same compiler, same version, perhaps, more
>>>>> "memory". I think I am not alone in this...
>>>>>
>>>> Why?
>>> There are many possible *valid* reasons for this. One is that if you are
>>> not using the same version of the same compiler with the same switches
>>> then the code you are testing is not the same as the code that will be
>>> run. Since compilers *do* have bugs it is possible that the bug will be
>>> triggered in the real environment but not in the test environment unless
>>> you ensure that they are the same.
>>>
>> But one has to differentiate between developer unit testing (the subject
>> of this post) and QA (customer) acceptance testing.
>
> You have missed out internal formal testing which in many environments
> is far more complete than acceptance testing. For example, I've worked
> on projects where a formal test literally takes a week to complete but
> the customer acceptance testing takes only a few hours.
>
If performed, internal formal testing is still a step away from
developer testing.

>> The former can be
>> performed on any environment the developer chooses,
>
> Informal testing can be run in any environment the developer has
> available. Formal testing, which is the only sort of testing that you
> can guarantee will be available and working for those maintaining later,
> is another matter.
>
How so? A unit test suite doesn't just vanish when the code is
released, it is an essential part of the code base.
>>
>> Again, this is different from developer unit testing, I don't think
>> anyone would be daft enough to release a product that hadn't been
>> through acceptance testing on the target platform.
>
> Acceptance testing has very little to do with proving whether the system
> works, it is just to give the customer some confidence.

That depends on your definition of Acceptance tests. In our case, they
are the automated suite of tests that have to pass before the product is
released to customers.

> The real worth
> while formal testing has to be completed *before* doing customer
> acceptance testing and done with the correct compiler. At least, this is
> the case in many environments, including all the projects where I have
> been involved in QA, and on the safety critical project I was involved in.
>
Again, that depends on your process.

> If your customer acceptance testing is sufficient to prove the SW is
> sufficiently correct then your customer has either very little trust in
> your company or a lot of time to waste. If your customer acceptance
> testing is the only testing done with the correct compiler and it is not
> sufficient to prove your SW is sufficiently correct then your SW is not
> tested properly. At least, not according to any standard of testing I
> have come across.

Why? Our acceptance test are very comprehensive, written by
professional testers working with a product manager (the customer).

It sounds like you don't have fully automated acceptance tests. Where
ever possible, all tests should be fully automated.

--
Ian Collins.

Ben Bacarisse said:

<snip>
>
> I suspect that [DEK] is not entirely happy with the way that quip
> is used so often to suggest the pointlessness of proofs[2]

<snip>

> [2] This not one of those times -- RH was just countering the much
> stronger assertion that proof => no need to test.

Right. One problem is that they don't always prove what you asked them
to prove. What you actually want to know is "does this program properly
do what I need it to do?", but what a prover actually tells you is
whether program X conforms to a particular expression of specification
Y. It makes no comment whatsoever on whether specification Y
corresponds to wishlist Z. And, very often, such correspondence is far
from perfect.

--
Richard Heathfield <http://www.cpax.org.uk>
Email: -www. +rjh@
Google users: <http://www.cpax.org.uk/prg/writings/googly.php>
"Usenet is a strange place" - dmr 29 July 1999

On Mon, 27 Aug 2007 19:14:04 +1200, Ian Collins <ian-news@hotmail.com>
wrote:

><snip>
>> The farthest I can go away from the target is a software simulator of
>> the instruction set. Same compiler, same version, perhaps, more
>> "memory". I think I am not alone in this...
>>
>Why?

Perhaps because this is an example of a medical product where that is
felt to be required. There is a list of various kinds of "structural
coverages," those selected commensurate with the level of risk posed
by the software. (Saying something has "coverage," I think, always
implies 100% coverage, too. Not partial. So you either have coverage
or you don't.)

Borrowing from one of the US CDRH PDFs I have laying about:

· Statement Coverage – This criteria requires sufficient test cases
for each program statement to be executed at least once; however,
its achievement is insufficient to provide confidence in a
software product's behavior.

· Decision (Branch) Coverage – This criteria requires sufficient test
cases for each program decision or branch to be executed so that
each possible outcome occurs at least once. It is considered to be
a minimum level of coverage for most software products, but
decision coverage alone is insufficient for high-integrity
applications.

· Condition Coverage – This criteria requires sufficient test cases
for each condition in a program decision to take on all possible
outcomes at least once. It differs from branch coverage only when
multiple conditions must be evaluated to reach a decision.

· Multi-Condition Coverage – This criteria requires sufficient test
cases to exercise all possible combinations of conditions in a
program decision.

· Loop Coverage – This criteria requires sufficient test cases for
all program loops to be executed for zero, one, two, and many
iterations covering initialization, typical running and termination
(boundary) conditions.

· Path Coverage – This criteria requires sufficient test cases for
each feasible path, basis path, etc., from start to exit of a
defined program segment, to be executed at least once. Because of
the very large number of possible paths through a software program,
path coverage is generally not achievable. The amount of path
coverage is normally established based on the risk or criticality
of the software under test.

· Data Flow Coverage – This criteria requires sufficient test cases
for each feasible data flow to be executed at least once. A number
of data flow testing strategies are available.

For potentially high risk software, you may not just use a different
compiler or a different operating system environment or change even
the optimization options. As the OP mentioned, it's probably going to
enough just justifying an instruction simulator.

I can easily see a desire for an automated way of demonstrating that
structural testing has achieved one or more of these cases. If I read
the OP right about this, anyway.

Jon

Ben Bacarisse <ben.usenet@bsb.me.uk> wrote:

> Richard Heathfield <rjh@see.sig.invalid> writes:
>
> > Ben Bacarisse said:
> >
> >> Richard Heathfield <rjh@see.sig.invalid> writes:
> >>
> >>> Erik Wikström said:
> >>>
> >>>> Testing is used to find errors, while formal methods are used to
> >>>> prove that there are no errors, at least that's the goal. So if you
> >>>> can prove that there are no errors why test for them?
> >>>
> >>> "Beware of bugs in the above code; I have only proved it correct, not
> >>> tried it." - Donald E Knuth.
> >>
> >> But this was a "by hand" proof in 1977. A machine assisted proof of
> >> the actual code could be expected to inspire a little more confidence.
> >
> > Why? Presumably the machine that is doing the assisting is itself a
> > computer program. What makes you think the assistance program is
> > correct?
>
> What do you test your software with if not more software?

Sed quis custodiet ipsos custodes?

Richard

Jonathan Kirwan wrote:
> On Mon, 27 Aug 2007 19:14:04 +1200, Ian Collins <ian-news@hotmail.com>
> wrote:
>
>> <snip>
>>> The farthest I can go away from the target is a software simulator of
>>> the instruction set. Same compiler, same version, perhaps, more
>>> "memory". I think I am not alone in this...
>>>
>> Why?
>
> Perhaps because this is an example of a medical product where that is
> felt to be required. There is a list of various kinds of "structural
> coverages," those selected commensurate with the level of risk posed
> by the software. (Saying something has "coverage," I think, always
> implies 100% coverage, too. Not partial. So you either have coverage
> or you don't.)
>
The why was prompted by the posting subject "critique of a C unit test
environment". To my way of thinking (TDD), unit tests are developer
tool, not formal product tests.


<interesting stuff snipped>


--
Ian Collins.