What is the Name of the Problem or Technique of Determining if a Line in a Program Will Execute

Question

If I were to pose the question: "Given a program $P$ containing statement $X$, will $X$ be executed (given enough runs with all possible inputs)?"

This strikes me of being a relative of the Halting Problem, but I just don't know the taxonomy here.

What is the name of this problem, or does it not have a name because it is solved/uninteresting?

Answer 1

This is called the reachability problem -- is it possible for a given system to enter a given state?

Techniques that attempt to answer this problem fall under reachability analysis, which is one of the main goals of (finite / symbolic) model checking.

---

As the other answer suggests, this is one of the many instances covered by Rice's theorem. Answering questions about the runtime behavior of programs from only their source code is almost always undecidable. Nonetheless, there are many attempts to solve these problems that can be fairly effective in "real world" code (e.g., Microsoft's 2002 project SLAM), because human programmers tend to try to make their code easy to understand (for other humans; we hope incidentally also for mechanical analysis)

Answer 2

EDIT: This answer is more detailed than mine.

This is an example of a question covered by Rice's theorem. For example, the question of if a program outputs "Hello World" or not is covered by that theorem.

It also covers quantification over inputs (e.g. does program $P$ do $X$ on all input, does program $P$ do $X$ on some inputs, does program $P$ do $X$ on even inputs, etc...).

In particular, it states that in general, the problem is only semidecidable, just like the Halting problem.

EDIT: The theorem is only about what a program does, not its internals. So the question of "does a program ever get to line 7?" technically is not covered by the theorem. To get around this, just imagine that your interpreter/compiler prints out the line number it is currently on. Now the question is "does the program ever say it is on line 7?", which is a question about what it does, and therefore covered by Rice's theorem. You do not need to actually make the modification; just proving the possibility is enough.

Answer 3

Several others have pointed to Rice's Theorem as an answer proving that this is undecidable. As a trivial alternative to that line of reasoning, your problem statement can be shown to be isomorphic to a straight forward halting problem.

To do this, transform the program using the following rules:

• The statement X is replaced with a statement which halts.
• All other statement which halt are replaced with an infinite loop
• An infinite loop is appended to the end of the program (if the end is not already considered to be a statement which halts)

It's trivial to see that solving the halting problem for this transformed problem is identical to determining if X is reachable in the original program. Thus, said reachability is undecidable in general.