3 ms·

I would say both are correct. From a psychological\SE standpoint know your faults and develop defenses for them. That could be use a language that doesn't allo

I would say both are correct. From a psychological\SE standpoint know your faults and develop defenses for them. That could be use a language that doesn't allow them to even be thought in the first place, or develop defensive coding standards that prevent them. But that answer is more stochastic, it helps but anything short of formal proof is just raising the likely hood of success not a guarantee. I also wonder if a static analysis tool would have caught the bug. Are there any good static analysis tools for Java or Python that might have caught the bug without the overhead of writing the formal proof?

tomp 12y ago
As I understand, they didn't write a formal proof, but only the pre- and post-conditions, along with loop invariants. The formal proof was then completed by automatic theorem provers. There has been some research into contracts inference, but with very limited results. Even if you added all the pre- and post-conditions manually, I'm not sure loop invariants could be inferred (especially as they can get pretty complex).
- stonemetal 12y ago
  True, I more meant their method required O(n) effort since they had to write pre\post conditions and invariant for the tool. Whereas something like codeSonar or PVS Studio requires O(1) effort, just point it at your build and press go. The bug they found was an implementation defect, something I believe the low effort tools would have caught. Where their tool should shine would be in detecting something the low effort analysis tools miss.
  - saidajigumi 12y ago
    > something I believe the low effort tools would have caught. It's worth noting that the formal verification method brought to light the root cause, where prior attempts at fixing this bug in TimSort had merely made it less common. Would codeSonar or PVS Studio actually have provided the insight, in "O(1)", required to fix the root cause? I'm not familiar with those tools, but I sincerely doubt it.
- qznc 12y ago
  Working with KeY is similar to writing a proof. The development of pre-, post-conditions and invariants is done interactively with the theorem prover, which shows you what is missing.

tomp 12y ago

As I understand, they didn't write a formal proof, but only the pre- and post-conditions, along with loop invariants. The formal proof was then completed by automatic theorem provers. There has been some research into contracts inference, but with very limited results. Even if you added all the pre- and post-conditions manually, I'm not sure loop invariants could be inferred (especially as they can get pretty complex).

stonemetal 12y ago
True, I more meant their method required O(n) effort since they had to write pre\post conditions and invariant for the tool. Whereas something like codeSonar or PVS Studio requires O(1) effort, just point it at your build and press go. The bug they found was an implementation defect, something I believe the low effort tools would have caught. Where their tool should shine would be in detecting something the low effort analysis tools miss.
- saidajigumi 12y ago
  > something I believe the low effort tools would have caught. It's worth noting that the formal verification method brought to light the root cause, where prior attempts at fixing this bug in TimSort had merely made it less common. Would codeSonar or PVS Studio actually have provided the insight, in "O(1)", required to fix the root cause? I'm not familiar with those tools, but I sincerely doubt it.
qznc 12y ago
Working with KeY is similar to writing a proof. The development of pre-, post-conditions and invariants is done interactively with the theorem prover, which shows you what is missing.