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












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?










share|cite|improve this question











$endgroup$

















    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?










    share|cite|improve this question











    $endgroup$















      3












      3








      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?










      share|cite|improve this question











      $endgroup$




      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?







      computability terminology rice-theorem






      share|cite|improve this question















      share|cite|improve this question













      share|cite|improve this question




      share|cite|improve this question








      edited Jan 24 at 5:58









      Apass.Jack

      12.5k1939




      12.5k1939










      asked Jan 22 at 18:39









      Keenan DiggsKeenan Diggs

      1183




      1183






















          3 Answers
          3






          active

          oldest

          votes


















          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)






          share|cite|improve this answer









          $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.






            share|cite|improve this answer











            $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.






            share|cite|improve this answer









            $endgroup$













              Your Answer





              StackExchange.ifUsing("editor", function () {
              return StackExchange.using("mathjaxEditing", function () {
              StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
              StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
              });
              });
              }, "mathjax-editing");

              StackExchange.ready(function() {
              var channelOptions = {
              tags: "".split(" "),
              id: "419"
              };
              initTagRenderer("".split(" "), "".split(" "), channelOptions);

              StackExchange.using("externalEditor", function() {
              // Have to fire editor after snippets, if snippets enabled
              if (StackExchange.settings.snippets.snippetsEnabled) {
              StackExchange.using("snippets", function() {
              createEditor();
              });
              }
              else {
              createEditor();
              }
              });

              function createEditor() {
              StackExchange.prepareEditor({
              heartbeatType: 'answer',
              autoActivateHeartbeat: false,
              convertImagesToLinks: false,
              noModals: true,
              showLowRepImageUploadWarning: true,
              reputationToPostImages: null,
              bindNavPrevention: true,
              postfix: "",
              imageUploader: {
              brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
              contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
              allowUrls: true
              },
              onDemand: true,
              discardSelector: ".discard-answer"
              ,immediatelyShowMarkdownHelp:true
              });


              }
              });














              draft saved

              draft discarded


















              StackExchange.ready(
              function () {
              StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f103247%2fwhat-is-the-name-of-the-problem-or-technique-of-determining-if-a-line-in-a-progr%23new-answer', 'question_page');
              }
              );

              Post as a guest















              Required, but never shown

























              3 Answers
              3






              active

              oldest

              votes








              3 Answers
              3






              active

              oldest

              votes









              active

              oldest

              votes






              active

              oldest

              votes









              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)






              share|cite|improve this answer









              $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)






                share|cite|improve this answer









                $endgroup$
















                  8












                  8








                  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)






                  share|cite|improve this answer









                  $endgroup$



                  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)







                  share|cite|improve this answer












                  share|cite|improve this answer



                  share|cite|improve this answer










                  answered Jan 23 at 0:20









                  Curtis FCurtis F

                  449211




                  449211























                      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.






                      share|cite|improve this answer











                      $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
















                      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.






                      share|cite|improve this answer











                      $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














                      5












                      5








                      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.






                      share|cite|improve this answer











                      $endgroup$



                      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.







                      share|cite|improve this answer














                      share|cite|improve this answer



                      share|cite|improve this answer








                      edited Jan 23 at 0:31

























                      answered Jan 22 at 18:48









                      PyRulezPyRulez

                      398117




                      398117












                      • $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


















                      • $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
















                      $begingroup$
                      Thank you for answering my question. I will continue my research toward Rice's Theorem.
                      $endgroup$
                      – Keenan Diggs
                      Jan 22 at 19:30




                      $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




                      1




                      $begingroup$
                      @KeenanDiggs if you have any other questions, let me know.
                      $endgroup$
                      – PyRulez
                      Jan 22 at 19:31




                      $begingroup$
                      @KeenanDiggs if you have any other questions, let me know.
                      $endgroup$
                      – PyRulez
                      Jan 22 at 19:31




                      1




                      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






                      $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




                      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




                      $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




                      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




                      $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.






                      share|cite|improve this answer









                      $endgroup$


















                        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.






                        share|cite|improve this answer









                        $endgroup$
















                          1












                          1








                          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.






                          share|cite|improve this answer









                          $endgroup$



                          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.







                          share|cite|improve this answer












                          share|cite|improve this answer



                          share|cite|improve this answer










                          answered Jan 23 at 3:39









                          Cort AmmonCort Ammon

                          2,614813




                          2,614813






























                              draft saved

                              draft discarded




















































                              Thanks for contributing an answer to Computer Science Stack Exchange!


                              • Please be sure to answer the question. Provide details and share your research!

                              But avoid



                              • Asking for help, clarification, or responding to other answers.

                              • Making statements based on opinion; back them up with references or personal experience.


                              Use MathJax to format equations. MathJax reference.


                              To learn more, see our tips on writing great answers.




                              draft saved


                              draft discarded














                              StackExchange.ready(
                              function () {
                              StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f103247%2fwhat-is-the-name-of-the-problem-or-technique-of-determining-if-a-line-in-a-progr%23new-answer', 'question_page');
                              }
                              );

                              Post as a guest















                              Required, but never shown





















































                              Required, but never shown














                              Required, but never shown












                              Required, but never shown







                              Required, but never shown

































                              Required, but never shown














                              Required, but never shown












                              Required, but never shown







                              Required, but never shown







                              Popular posts from this blog

                              MongoDB - Not Authorized To Execute Command

                              in spring boot 2.1 many test slices are not allowed anymore due to multiple @BootstrapWith

                              How to fix TextFormField cause rebuild widget in Flutter