This is a question that arose when studying Rice's theorem. As you all might know, Rice's theorem (informally and simply) states:
"There is no Turing machine (i.e. program) that can always (or generally) decide whether the language of another given Turing machine (i.e. program) satisfies a particular nontrivial property".
Some real examples of these nontrivial properties are:
- Does a given program eventually halt for all possible inputs? (Turing's halting problem)
- Are all accesses to an array in a given program inside the array's bounds? (buffer-overflow/overrun)
- Is a given C program free of "use-after-free" bugs? (using a pointer after releasing it)
But there are also some other nontrivial properties for programs that can be decided using other programs (for example, compilers):
- Are all the function invocations in a program previously defined? (Detecting undefined function invocations)
- Are all the variables in a program initialized?
- Do all assignment operations in a program, satisfy type-safety? (Detecting incompatible types assignments)
So it seems that not all nontrivial properties are the subject of Rice's undecidability theorem. An explanation in the Wikipedia article states:
"It is important to note that Rice's theorem does not say anything about those properties of machines or programs that are not also properties of functions and languages."
Unfortunately, this explanation didn't exactly help me understand the distinguishing aspect of properties that are subject of Rice's theorem from those properties that aren't.
Further down the Wikipedia article, it restates the matter like this:
"There exists no automatic method that decides with generality non-trivial questions on the behavior of computer programs."
My speculation from the term "program behavior", and additionally by observing the example properties, is that any nontrivial property that is related to the program's runtime data, is the subject of Rice's theorem (e.g. array indexing, pointer lifetime, halting, ...). In contrast, properties that are unrelated to the program's runtime data are not subject to Rice's theorem (e.g. type-safety, function definitions, variable initialization, ...). Note that I'm assuming "variable initialization" to be static data, not dynamic runtime data.
How correct or accurate is my speculation? If I'm mistaken then, is there an intuitive and concise explanation on the distinguishing aspects of properties that are subject to Rice's theorem from those that are not?
By "intuitive and concise" I mean an explanation suitable for a one session presentation of Rice's theorem to an audience of higher-undergrads and grad students of CS.