3 ms·
Yes, I'd forgotten that bit already... But I don't know how you can check that without running it for anything but the most trivial programs.
by wccrawford 15y ago
Yes, I'd forgotten that bit already... But I don't know how you can check that without running it for anything but the most trivial programs.
- andrewflnr 15y agoOops. Fixed. There is a fair bit of theory about static verification/analysis of programs, a lot of which is applied in optimizing compilers as well. I'm not familiar with it, but I imagine that in this case it just fails on anything less than positive proof, and is comfortable with the strict standard that imposes. It talks more about constraints here: http://whiley.org/guide/constraints/ http://whiley.org/guide/constraints/ .
- fmap 15y agoYou are right, the problem is undecidable in general. If the compiler is unsure whether a constraint is satisfied it will have to add a runtime check. This is similar to the behavior of array accesses in Java: If you access an invalid index the JVM is required to throw an out of bounds exception. In practice this would be unacceptably slow and if the compiler can prove that such an exception can never happen, the check will be removed. As for the "simple" example of testing "y == 0", this is actually already undecidable. If you are interested, you might have a look at Nielson's "Principles of Program Analysis", I think that this particular example (undecidability of MOP Constant Propagation) is worked out there. Also, the book is a nice introduction to the subject.
- redjamjar 15y agoThe good news about undecidability is that, for the most part, it's not a problem. That is, the problem instances that arise in practice are almost never actually undecidable.