Walter: > BTW, a while back Spec# was touted here as having this great theorem contract > prover, and what a great tool that was. Reading the documentation on it, it > looked great. So I tried it out in pastebin. It pretty much only works on the > examples given in the marketing literature. It couldn't even handle bitwise > ops.
You are missing something important. The purpose of Spec# (and newer things that are coming out now) is to create a small kernel (for an operating system) that is 100% proved correct (correct according to its specs, etc). If they don't use an automatic theorem prover, then they have to do 100% of the proofs by hand. Even if the tool is able to do only 30% of the proofs automatically (and another 40% with a bit of help) it's a lot of manual work saved. The papers report the percentage of the theorems done by the tool, the percentage of the theorems done partially by hand, and the remaining percentage done by hand. The source code is all available, to verify the numbers inside the papers are not made up. > I know enough about data flow analysis to infer what clang is doing from its > pattern of reports, and it hasn't even begun to solve this problem. Clang static analysis is a very new sub-tool. On the market there are commercial lint tools that are probably 15-18 times older than Clang. Give Clang two or three years are we'll see. Its creators have created a good C++ compiler in a very short time, and its back-end is already rivalling GCC in optimizations (it's not there yet, but the distance is not so much, auto-vectorization is one of the most important differences between the two back-ends). Bye, bearophile
