Re: Transactions: good or bad?

"Todd Bandrowsky" <anakin_at_unitedsoftworks.com> wrote in message news:af3d9224.0306101020.28065bb7_at_posting.google.com...
> Um, imagine if you will you had a technology that could lift out all
> of your decision logic, and drop it into a tree. Given that, and a
> call graph, you could back generate test cases to ensure 100% complete
> coverage. If, each one of those cases yields correct behavior, is not
> the program formally proved?

Absolutely not. It may still be riddled with bugs. I demonstrated a simple example of this in an earlier posting in this thread. Code coverage is nice and all, but it does not lead you to something as strong as a proof.

> I'm not saying that dropping random data onto an application is a
> formal proof. I'm saying that an application contains the information
> with which a complete coverage of test cases could be theoretically
> constructed, and, if you had that construction, you could then pair
> that up with a database of previously proved results and thus validate
> your application.

This only works if your test coverage includes every possible set of inputs. This is generally prohibitive. For example, to exhaustively test the unix "sort" program, you would have to construct every possible input file, (up to the maximum size the filesystem supported, perhaps 2^64 bytes) and also construct a sorted version of each such file. Then you run sort on each input file and verify that it produces the appropriate the output file. That would be equivalent to a proof. Note that an actual proof of the program would be substantially easier.

Marshall Received on Wed Jun 11 2003 - 08:26:20 CEST