Preuve que le code mort ne peut pas être détecté par les compilateurs

Je prévois d'enseigner un cours d'hiver sur un nombre variable de sujets, dont l'un sera les compilateurs. Maintenant, je suis tombé sur ce problème en pensant aux affectations à donner tout au long du trimestre, mais cela m'a déconcerté, je pourrais donc l'utiliser à titre d'exemple.

public class DeadCode {
  public static void main(String[] args) {
     return;
     System.out.println("This line won't print.");
  }
}

Dans le programme ci-dessus, il est évident que l'instruction print ne s'exécutera jamais à cause de return. Les compilateurs donnent parfois des avertissements ou des erreurs concernant le code mort. Par exemple, le code ci-dessus ne se compilera pas en Java. Cependant, le compilateur javac ne détectera pas toutes les instances de code mort dans chaque programme. Comment pourrais-je prouver qu'aucun compilateur ne peut le faire?

Tout cela vient de l'indécidabilité du problème de l'arrêt. Supposons que nous ayons une fonction de code mort "parfait", une machine de Turing M et une chaîne d'entrée x, et une procédure qui ressemble à ceci:

Run M on input x;
print "Finished running input";

Si M s'exécute pour toujours, nous supprimons l'instruction print, car nous ne l'atteindrons jamais. Si M ne s'exécute pas indéfiniment, nous devons conserver l'instruction print. Ainsi, si nous avons un suppresseur de code mort, il nous permet également de résoudre le problème d'arrêt, nous savons donc qu'il ne peut pas y avoir un tel suppresseur de code mort.

Nous pouvons contourner ce problème par «approximation conservatrice». Donc, dans mon exemple de Turing Machine ci-dessus, nous pouvons supposer que l'exécution de M sur x peut se terminer, donc nous le faisons en toute sécurité et ne supprimons pas l'instruction d'impression. Dans votre exemple, nous savons que, quelles que soient les fonctions qui s'arrêtent ou non, il n'y a aucun moyen d'atteindre cette instruction d'impression.

Habituellement, cela se fait en construisant un "graphique de flux de contrôle". Nous faisons des hypothèses simplificatrices, telles que "la fin d'une boucle while est connectée au début et à l'instruction après", même si elle s'exécute pour toujours ou ne s'exécute qu'une seule fois et ne visite pas les deux. De même, nous supposons qu'une instruction if peut atteindre toutes ses branches, même si en réalité certaines ne sont jamais utilisées. Ces types de simplifications nous permettent de supprimer le "code manifestement mort" comme l'exemple que vous donnez, tout en restant décidable.

Pour clarifier quelques confusions des commentaires:

1. Nitpick: pour M fixe, c'est toujours décidable. M doit être l'entrée

   Comme le dit Raphaël, dans mon exemple, nous considérons la machine de Turing comme une entrée. L'idée est que, si nous avions un algorithme DCE parfait, nous serions en mesure de construire l'extrait de code que je donne pour n'importe quelle machine de Turing , et avoir un DCE résoudrait le problème d'arrêt.

2. pas convaincu. retourner comme une instruction franche dans une exécution directe sans branche n'est pas difficile à décider. (et mon compilateur me dit qu'il est capable de comprendre cela)

   Pour le problème soulevé par njzk2: vous avez absolument raison, dans ce cas, vous pouvez déterminer qu'il n'y a aucun moyen d'obtenir une déclaration après le retour. Cela est dû au fait qu'il est suffisamment simple pour décrire son inaccessibilité à l'aide de contraintes de graphique de flux de contrôle (c'est-à-dire qu'il n'y a pas de fronts sortants d'une déclaration de retour). Mais il n'y a pas d'éliminateur de code mort parfait, ce qui élimine tout le code inutilisé.

3. Je ne prends pas de preuve dépendante de l'entrée pour une preuve. S'il existe un tel type d'entrée utilisateur qui peut permettre au code d'être fini, il est correct pour le compilateur de supposer que la branche suivante n'est pas morte. Je ne vois pas à quoi servent tous ces votes positifs, c'est à la fois évident (par exemple stdin sans fin) et faux.

   Pour TomášZato: ce n'est pas vraiment une preuve dépendante de l'entrée. Interprétez-le plutôt comme un "forall". Cela fonctionne comme suit: supposons que nous avons un algorithme DCE parfait. Si vous me donnez une machine de Turing M arbitraire et saisissez x, je peux utiliser mon algorithme DCE pour déterminer si M s'arrête, en construisant l'extrait de code ci-dessus et en voyant si l'instruction d'impression est supprimée. Cette technique, consistant à laisser un paramètre arbitraire pour prouver une instruction forall, est courante en mathématiques et en logique.

   Je ne comprends pas bien le point de TomášZato sur le code étant fini. Certes, le code est fini, mais un algorithme DCE parfait doit s'appliquer à tout le code, qui est un ensemble infini. De même, alors que le code lui-même est fini, les ensembles potentiels d'entrée sont infinis, tout comme le temps d'exécution potentiel du code.

   Quant à considérer que la branche finale n'est pas morte: elle est sûre en termes d '"approximation conservatrice" dont je parle, mais ce n'est pas suffisant pour détecter toutes les instances de code mort comme l'OP le demande.

Considérez le code comme ceci:

while (true)
  print "Hello"
print "goodbye"

De toute évidence, nous pouvons supprimer print "goodbye"sans modifier le comportement du programme. C'est donc du code mort. Mais s'il y a un appel de fonction différent au lieu de (true)dans la whilecondition, alors nous ne savons pas si nous pouvons le supprimer ou non, conduisant à l'indécidabilité.

Notez que je ne propose pas cela tout seul. C'est un résultat bien connu dans la théorie des compilateurs. Il en est question dans The Tiger Book . (Vous pourrez peut-être voir de quoi ils parlent dans Google Books .

Ceci est une variante de la réponse de jmite qui contourne la confusion potentielle concernant la non-résiliation. Je vais donner un programme qui s'arrête toujours, peut avoir du code mort mais nous ne pouvons pas (toujours) décider de manière algorithmique si c'est le cas.

Considérez la classe d'entrées suivante pour l'identificateur de code mort:

simulateMx(n) {
  simulate TM M on input x for n steps
  if M did halt
    return 0
  else
    return 1
}

Depuis Met xsont fixes, simulateMsa un code mort avec return 0si et seulement si Mne s'arrête pas x.

Cela nous donne immédiatement une réduction du problème d'arrêt à la vérification du code mort: étant donné TM comme instance de problème d'arrêt, créez le programme ci-dessus avec le code de - il a du code mort si et seulement si ne s'arrête pas tout seul code.M $M$x$M$$M$

Par conséquent, la vérification du code mort n'est pas calculable.

Dans le cas où vous n'êtes pas familier avec la réduction comme technique de preuve dans ce contexte, je recommande notre matériel de référence .

Un moyen simple de démontrer ce type de propriété sans être embourbé dans les détails est d'utiliser le lemme suivant:

Lemme: Pour tout compilateur C pour un langage Turing-complet, il existe une fonction undecidable_but_true()qui ne prend aucun argument et renvoie le booléen true, de sorte que C ne peut pas prédire si undecidable_but_true()retourne vrai ou faux.

Notez que la fonction dépend du compilateur. Étant donné une fonction undecidable_but_true1(), un compilateur peut toujours être augmenté en sachant si cette fonction renvoie vrai ou faux; mais il y a toujours une autre fonction undecidable_but_true2()qui ne sera pas couverte.

Preuve: selon le théorème de Rice , la propriété «cette fonction retourne vraie» est indécidable. Par conséquent, aucun algorithme d'analyse statique ne peut décider de cette propriété pour toutes les fonctions possibles.

Corollaire: étant donné un compilateur C, le programme suivant contient du code mort qui ne peut pas être détecté:

if (!undecidable_but_true()) {
    do_stuff();
}

Une note à propos de Java: le langage Java exige que les compilateurs rejettent certains programmes qui contiennent du code inaccessible, tout en exigeant de manière raisonnable que le code soit fourni à tous les points accessibles (par exemple, le flux de contrôle dans une fonction non vide doit se terminer par une returninstruction). Le langage spécifie exactement comment l'analyse de code inaccessible est effectuée; sinon, il serait impossible d'écrire des programmes portables. Étant donné un programme du formulaire

some_method () {
    <code whose continuation is unreachable>
    // is throw InternalError() needed here?
}

il est nécessaire de spécifier dans quels cas le code inaccessible doit être suivi d'un autre code et dans quels cas il ne doit être suivi d'aucun code. Un exemple de programme Java contenant du code inaccessible, mais pas d'une manière que les compilateurs Java sont autorisés à remarquer, apparaît dans Java 101:

String day_of_week(int n) {
    switch (n % 7) {
    case 0: return "Sunday";
    case 1: case -6: return "Monday";
    …
    case 6: case -1: return "Saturday";
    }
    // return or throw is required here, even though this point is unreachable
}

La réponse de jmite s'applique à savoir si le programme quittera jamais un calcul - simplement parce qu'il est infini, je n'appellerais pas le code après sa mort.

Cependant, il existe une autre approche: un problème pour lequel il existe une réponse mais inconnue:

public void Demo()
{
  if (Chess.Evaluate(new Chessboard(), int.MaxValue) != 0)
    MessageBox.Show("Chess is unfair!");
  else
    MessageBox.Show("Chess is fair!");
}

public class chess
{
  public Int64 Evaluate(Chessboard Board, int SearchDepth)
  {
  ...
  }
}

Cette routine sans aucun doute ne contient le code mort - la fonction renvoie une réponse qui exécute un chemin , mais pas l'autre. Bonne chance pour le trouver! Ma mémoire est qu'aucun ordinateur théorique ne peut résoudre ce problème pendant la durée de vie de l'univers.

Plus en détail:

La Evaluate()fonction calcule quel côté gagne un jeu d'échecs si les deux côtés jouent parfaitement (avec une profondeur de recherche maximale).

Les évaluateurs d'échecs regardent normalement à chaque déplacement possible une profondeur spécifiée, puis tentent de marquer le plateau à ce point (parfois, étendre certaines branches plus loin, car regarder à mi-chemin dans un échange ou similaire peut produire une perception très asymétrique.) Étant donné que la profondeur maximale réelle soit 17695 demi-coups la recherche est exhaustive, elle parcourra tous les échecs possibles. Étant donné que tous les jeux se terminent, il n'est pas question d'essayer de décider de la qualité d'une position de chaque plateau (et donc pas de raison de regarder la logique d'évaluation du plateau - elle ne sera jamais appelée), le résultat est soit une victoire, une perte ou un tirage au sort. Si le résultat est un match nul, le jeu est équitable, si le résultat n'est pas un match nul, c'est un jeu injuste. Pour l'étendre un peu, nous obtenons:

public Int64 Evaluate(Chessboard Board, int SearchDepth)
{
  foreach (ChessMove Move in Board.GetPossibleMoves())
    {
      Chessboard NewBoard = Board.MakeMove(Move);
      if (NewBoard.Checkmate()) return int.MaxValue;
      if (NewBoard.Draw()) return 0;
      if (SearchDepth == 0) return NewBoard.Score();
      return -Evaluate(NewBoard, SearchDepth - 1);
    }
}

Notez également qu'il sera pratiquement impossible pour le compilateur de réaliser que Chessboard.Score () est du code mort. Une connaissance des règles des échecs nous permet aux humains de comprendre cela, mais pour le comprendre, vous devez savoir que MakeMove ne peut jamais augmenter le nombre de pièces et que Chessboard.Draw () retournera vrai si le nombre de pièces reste statique pendant trop longtemps. .

Notez que la profondeur de recherche est en demi-coups, pas en mouvements entiers. C'est normal pour ce type de routine AI car c'est une routine O (x ^ n) - l'ajout d'un pli de recherche supplémentaire a un effet majeur sur la durée d'exécution.

Je pense que dans un cours d'informatique, la notion de code mort est intéressante dans le contexte de la compréhension de la différence entre le temps de compilation et le temps d'exécution!

Un compilateur peut déterminer quand vous avez du code qui ne peut en aucun cas être parcouru au moment de la compilation, mais il ne peut pas le faire pour l'exécution. une simple boucle while avec entrée utilisateur pour le test de rupture de boucle le montre.

Si un compilateur pouvait réellement déterminer le code mort à l'exécution (c.-à-d. Discerner Turing complet), alors il y a un argument selon lequel le code n'a jamais besoin d'être exécuté, car le travail est déjà fait!

Si rien d'autre, l'existence de code qui passe les vérifications de code mort à la compilation illustre la nécessité d'une vérification pragmatique des limites des entrées et d'une hygiène de codage générale (dans le monde réel des projets réels).