Debugging

A remark I have not heard about the last two posts is the following.

Pascal, how can you, in your last post claim that formal verification would have found the bug in your decimal-to-floating-point function? This is the kind of outrageous claim you rant against in your penultimate post! Formal verification did not find the bug. A code review did.

My answer is twofold. First subscribers get the blog they deserve. If you cannot rail and mock such obvious contradictions what is to prevent me from putting them in? Also I was not advertising a particular OCaml formal verification tool. I do not know any that accepts the full language. It was fully confident in the absence of any such tool that I claimed that if it existed and was usable and automatic enough to have actually been used it could have found the bug disclaimed in the last post. If provided with an appropriate specification. Which in the case at hand could only be a decimal-to-floating-point implementation in itself.

The truth is that Frama-C development involves a lot of old-fashioned testing and debugging. One factor is that available OCaml programmer-assistance tools do not always scale to projects the size of Frama-C. Another is that Frama-C uses some hard-to-get-right hard-to-diagnose techniques (for instance mixing data unmarshaling and hash-consing).

Speaking of which I think my Frama-C debugging colleagues will agree with me that this introduction to debugging is a nice read.