Re: Transactions: good or bad?

tj bandrowsky wrote:
>
> If I have lead you to believe that my analysis idea was strictly data
> based I am in error. In the back of my head I've been thinking expert
> systems type of an approach all the way. That is, use the logical
> assertions of the program to generate enough test data to test the
> other logical assertions, and let an operator / business owner check
> it against requirements. This is pie in the sky technology but this
> is a pie in the sky forum - "theory".

Your pie in the sky is provably impossible to cook :)

>
> To demonstrate a bad implementation of a function that is supposed to
> return true if and only if both a and b were true. It shows that you
> cannot just have a single set of inputs to this function. In our
> case, in fact, there are basically four inputs needed to test it, the
> permutations of a and b being true or false. But that is a long way
> from -every possible input-.
>
> So, instead of looking at just if - then elses, we would also need to
> have some understanding of how the language primitives work, in order
> to prove our application. From there, it seems reasonable to build
> an inference engine with the language primitives at its lowest level,
> and then use the program itself to add rules to that inference tree /
> knowledge base, whatever, and then, finally, have requirements that
> test all of the assertions made by the program to see if they are
> consistent. To do this in a meaningful way, and to be fairly strong
> about it, you need to have questions be asked so that every
> conditional / expression are hit at least once.
>
> In your above example, the testing engine would most certainly have to
> know about the behavior of a || b and understand that there needs to
> be four test cases, if the function is used only for conditional
> logic, and, some x number of more test cases depending on how it is
> used in other logic. An operator of the testing system could supply /
> override stuff.
>
> If people can make proofs, why can't computers?

To quote the great logician Jean-Yves Girard "a cause des ces fichues idees" (sorry for the lack of accents on my keyboard). In English it's "because of those bloody ideas" (that they totally do not have). For the whole delicious paper google on Jean-Yves Girard Les fondements des Mathematiques.

Plus, your whole logical construction, the pie in the sky sort to speak, is fundamentally unable to cope with non-determinism.

The bottom line is that proofs are better than test and for anything other than trivial cases a test is not a proof.

Test can only prove the presence of bugs, not their absence.

> While creating a
> proof may not be an algorithm, checking one most certainly is, is it
> not? Having a complex digital system be checked by a manual process
> on paper seems absurd and is there not a way formally verify systems?

Yes, there are. But it has nothing to do with your current claim (that you can exhaustively test computer programs).

> I know they did a lot of work on trying to get computers to write
> proofs for new things, but, for businesses, the relevant question is,
> will this code satisfy these requirements.

Yep, and they have totally failed to do that (getting computer to write proofs).

> Certainly requirements can
> be modelled as logical assertions.
>

Yep, and related to logical assertions, there are like tons of problems that are provably undecidable, impossible, NP-complete or otherwise infeasible.

Costin Received on Wed Jun 11 2003 - 19:55:39 CEST