>>8
0 bugs is an ideal, except for small programs. But you can work for approaching the minimum ammount of bugs. For that, TDD is the true path.
Name:
Anonymous2012-10-28 20:17
TDD is retarded. Prove or die.
Name:
Anonymous2012-10-28 20:28
>>9
I can see TEST DRIVE DEVELOPMENT increasing productivity of the developers, since it provides documentation for the expected behavior and an alert system for bugs that happen to become evident in one of the tests. But passing a series of test alone is not proof for correctness of the program. It helps if it can be verified that the tests exhaust every single logical path in the program.
If properties of the program can be proved with formal verification, those properties will hold as long as the assumptions made in the proofs hold. The issue then is describing every characteristic of the correct behavior. A theorem prover might be able to prove that a program will never index outside of an array, or access an invalid memory address, but it wont be able to tell you that it wont charge someone for a transaction twice unless you specifically as it to prove that for you. So it is possible for a verified program to have bugs if the bugs were not anticipated, and never proven impossible.
However, bugs like crashes from invalid memory access, running out of memory, or timing out, are absolutely unacceptable. These are bugs that can always be anticipated, thus they should always be proven to never occur.
Name:
Anonymous2012-10-28 20:52
if it can be turned into a test, it can and must be turned into a proof. documentation must be provided as postconditions and general idea, not as unit tests. software is buggy because of incompetent programmers doing TDD and similar crap, instead of proving.
>>14
fuck off back to the rest of the software industry, please.
Name:
Anonymous2012-10-28 22:20
>>14
I hate to contaminate my code with tests. I usually put tests on separate files and have them running at night everyday, and read the results first time in the morning.
This means that you write your tests first, create simple test-data at first and later populate this test-data with problematic cases, and run your full test suite everyday if possible. It makes programming complex system less annoying.
Name:
Anonymous2012-10-28 22:47
>>16
Think of the assertions as comments written in first order logic.
Dijkstra only wrote garbage. Why is he worshipped?
Name:
Anonymous2012-10-28 23:43
Aside From reviews of my books I have learned that many reviewers are annoyed by my closing brackets such as the above "(End of Legenda)", but they never give a convincing reason why I should depart from this convention, which, I think, is not without merit. So I shall stick to it. (End of Aside.)
both Church and Turing proved you cant prove programs to be correct due to the halting problem
Name:
Anonymous2012-10-29 0:38
>>24
The problem of constructing a proof that an arbitrary algorithm exhibits some property is undecidable. But the verification of an existing proof is decidable and can be done efficiently. If the proof of correctness is embedded into the language itself, then the program is its own definition and proof of correctness, which the compiler then verifies.
The problem is that whenever "proof" is mentioned it tends to immediately conjure up formal proofs like >>18, and that puts off a lot of programmers who wanted to prove their code was correct. Informal, but still methodical and logical proofs are much more valuable than tests. For example, in
p = malloc(...)
if(p) {
/* body */
}
it doesn't take much to prove that immediately upon entering the body, p is nonzero. And if you have a set of input values assumed to range [5..15], then adding 10 to the input value will let you know that the new range is [15..25].
Name:
Anonymous2012-10-29 2:50
Since Anders Hjellsberg created Typescript which gives Javascript static typing, I wonder if Typescript will be ported to other dynamically typed languages like Python and Ruby. That should eliminate a lot of testing that has to be done in dynamic languages