3
$\begingroup$

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?

$\endgroup$
8
$\begingroup$

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)

$\endgroup$
5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thank you for answering my question. I will continue my research toward Rice's Theorem. $\endgroup$ – Keenan Diggs Jan 22 at 19:30
  • 1
    $\begingroup$ @KeenanDiggs if you have any other questions, let me know. $\endgroup$ – PyRulez Jan 22 at 19:31
  • 1
    $\begingroup$ I downvoted this, because Rice's Theorem is not the name of the problem. It's the name of the theorem that you can't always solve the problem. The question asks, what is the problem called? $\endgroup$ – immibis Jan 23 at 4:50
  • 1
    $\begingroup$ @immibis I thought it's only name was "that problem Rice's theorem proves to be impossible". $\endgroup$ – PyRulez Jan 23 at 5:21
  • 1
    $\begingroup$ Impossible in general doesn't mean it's not useful to solve when it is possible. Programming teachers, for example, routinely figure out whether some code solves a particular problem. $\endgroup$ – immibis Jan 23 at 5:37
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.