On 7/29/2011 4:51 PM, bearophile wrote:
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.
From the way you originally positioned it, I had higher expectations.
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.
I think you misunderstand the scope of this problem. They've done data flow
analysis, an off-the-shelf technology for the last 30 years at least. They
haven't done any of the hard stuff that I can see.
It's like doing natural language translation using a dictionary. It looks like
it'll work, and you can have promising early success with it, but then you hit a
wall.
