Programmes théoriquement sans bogue

J'ai lu beaucoup d'articles qui déclarent que le code ne peut pas être exempt de bogues, et ils parlent de ces théorèmes:

• Arrêter le problème
• Théorème d'incomplétude de Gödel
• Théorème de Rice

En fait, le théorème de Rice ressemble à une implication du problème d'arrêt et le problème d'arrêt est en relation étroite avec le théorème d'incomplétude de Gödel.

Cela implique-t-il que chaque programme aura au moins un comportement involontaire? Ou cela signifie-t-il qu'il n'est pas possible d'écrire du code pour le vérifier? Qu'en est-il de la vérification récursive? Supposons que j'ai deux programmes. Les deux ont des bogues, mais ils ne partagent pas le même bogue. Que se passera-t-il si je les exécute simultanément?

Et bien sûr, la plupart des discussions ont porté sur les machines Turing. Qu'en est-il de l'automatisation linéaire (ordinateurs réels)?

Ce n'est pas tant que les programmes ne peuvent pas être exempts de bogues; c'est qu'il est très difficile de prouver qu'ils le sont, si le programme que vous essayez de prouver n'est pas trivial.

Pas faute d'essayer, faites attention. Les systèmes de type sont censés fournir une certaine assurance; Haskell a un système de type hautement sophistiqué qui le fait, dans une certaine mesure. Mais vous ne pouvez jamais supprimer toute l'incertitude.

Considérez la fonction suivante:

int add(int a, int b) { return a + b; }

Qu'est-ce qui pourrait mal tourner avec cette fonction? Je sais déjà à quoi tu penses. Disons que nous avons couvert toutes les bases, comme la vérification du débordement, etc. Que se passe-t-il si un rayon cosmique frappe le processeur, le faisant s'exécuter

LaunchMissiles();

au lieu?

OK, c'est peut-être un peu artificiel. Mais même des fonctions simples comme la addfonction ci-dessus doivent fonctionner dans des environnements où le processeur change constamment de contexte, basculant entre plusieurs threads et cœurs. Dans un tel environnement, tout peut arriver. Si vous en doutez, considérez que la RAM est fiable, non pas parce qu'elle est sans erreur, mais parce qu'elle a un système intégré pour corriger les erreurs de bits qui se produisent inévitablement.

Je sais ce que tu penses. "Mais je parle de logiciel, pas de matériel."

Il existe de nombreuses techniques qui peuvent améliorer votre niveau de confiance que le logiciel fonctionne comme il est censé le faire. La programmation fonctionnelle en fait partie. La programmation fonctionnelle vous permet de mieux raisonner sur la concurrence. Mais la programmation fonctionnelle n'est pas une preuve, pas plus que les tests unitaires.

Pourquoi? Parce que vous avez ces choses appelées cas de bord.

Et une fois que vous obtenez un peu au-delà de la simplicité de return a + b, il devient remarquablement difficile de prouver l'exactitude d'un programme.

Lectures complémentaires
Ils écrivent les bonnes choses
L'explosion d'Ariane 5

Tout d'abord, établissons le contexte dans lequel vous souhaitez en discuter. Les questions et réponses des programmeurs de Stack Exchange suggèrent que vous êtes très probablement intéressé par l' existence réelle des outils / langages plutôt que par les résultats théoriques et les théorèmes de l'informatique.

J'ai lu beaucoup d'articles qui déclarent que le code ne peut pas être exempt de bogues

J'espère que non, car une telle déclaration est incorrecte. Bien qu'il soit communément admis que la plupart des applications à grande échelle ne sont pas exemptes de bogues au meilleur de mes connaissances et de mon expérience.

Plus communément admis, il n'existe pas (c'est-à-dire l'existence, pas la possibilité) un outil qui détermine parfaitement si un programme écrit dans un langage de programmation complet de Turing est complètement exempt de bogues.

Une non-preuve est une extension intuitive du problème de l'arrêt, combinée avec les données d'observation de l'expérience quotidienne.

Il ne fait logiciel exist qui peut faire « preuves de correction » qui vérifient qu'un programme répond aux correspondants officiels spécifications du programme.

Cela implique-t-il que chaque programme aura au moins un comportement involontaire?

Non. Bien que la plupart des applications se soient révélées avoir au moins un bogue ou un comportement inattendu.

Ou cela signifie-t-il qu'il n'est pas possible d'écrire du code pour le vérifier?

Non, vous pouvez utiliser des spécifications formelles et des assistants de vérification pour vérifier le respect des spécifications , mais comme l'expérience l'a montré, des erreurs peuvent toujours exister dans le système global, telles que des facteurs extérieurs à la spécification - le traducteur de code source et le matériel, et le plus souvent, des erreurs sont commises dans les spécifications elles-mêmes.

Pour plus de détails sanglants, voir Coq est un tel outil / langage / système.

Qu'en est-il de la vérification récursive?

Je ne sais pas. Je ne le connais pas et je ne sais pas s'il s'agit d'un problème de calculabilité ou d'un problème d'optimisation du compilateur.

Je veux demander, cela implique-t-il que chaque code aura au moins un comportement involontaire?

Non. Des programmes corrects peuvent être et sont écrits. Attention, un programme peut être correct, mais son exécution peut échouer en raison, par exemple, de circonstances physiques (comme l'a écrit l'utilisateur Robert Harvey dans sa réponse ici ), mais c'est une question distincte: le code de ce programme est toujours correct. Pour être plus précis, l' échec n'est pas causé par une faute ou une erreur dans le programme lui-même, mais dans la machine sous-jacente qui l'exécute (*).

(*) J'emprunte des définitions de défaut , d' erreur et d' échec au champ de fiabilité comme, respectivement, un défaut statique, un état interne incorrect et un comportement observé externe incorrect selon ses spécifications (voir <tout article de ce champ>) .

Ou, cela signifie-t-il que je ne suis pas en mesure d'écrire du code, qui le vérifiera?

Référez-vous au cas général dans la déclaration ci-dessus et vous avez raison.

Vous pourrez peut-être écrire un programme qui vérifie si un programme X spécifique est correct. Par exemple, si vous définissez un programme "hello world" comme un programme avec deux instructions en séquence, à savoir print("hello world")et exit, vous pouvez écrire un programme qui vérifie si son entrée est un programme composé de ces deux instructions en séquence, indiquant ainsi s'il s'agit d'un programme "bonjour le monde" correct ou non.

Ce que vous ne pouvez pas faire en utilisant les formulations actuelles, c'est d'écrire un programme pour vérifier si un programme arbitraire s'arrête, ce qui implique l'impossibilité de tester l'exactitude dans les cas généraux.

L'exécution de deux variantes ou plus du même programme est une technique bien connue de tolérance aux pannes appelée programmation N-variante (ou N-version). Il s'agit d'une reconnaissance de la présence de bogues dans les logiciels.

Habituellement, ces variantes sont codées par différentes équipes de développement, à l'aide de différents compilateurs, et sont parfois exécutées sur différents CPU avec différents systèmes d'exploitation. Les résultats sont votés avant d'être transmis à l'utilisateur. Boeing et Airbus adorent ce type d'architecture.

Il reste deux liens faibles, ce qui entraîne des bogues en mode commun:

• Il n'y a qu'une seule spécification.
• le système de vote est unique ou complexe.

Un programme a des spécifications et s'exécute dans un environnement.

^{(l'exemple des rayons cosmiques dans d'autres réponses changeant adden FireMissiles pourrait être considéré comme faisant partie de "l'environnement")}

En supposant que vous pouvez spécifier formellement le comportement prévu du programme (c'est-à-dire sa spécification) et son environnement, vous pouvez parfois prouver formellement que le programme est - dans ce sens précis - exempt de bogues (donc son comportement ou sa sortie respecte la formalisation de sa spécification dans la formalisation de son environnement).

En particulier, vous pouvez utiliser des analyseurs de sources statiques sonores, comme par exemple Frama-C .

^{(mais l'état actuel de la technique de tels analyseurs ne permet pas l'analyse de programmes entiers et la preuve de programmes à grande échelle comme le compilateur GCC ou le navigateur Firefox ou le noyau Linux; et ma conviction est que de telles preuves ne se produiront pas de mon vivant Je suis né en 1959)}

Cependant, ce que vous avez prouvé, c'est le comportement correct du programme par rapport à certaines spécifications particulières dans certains environnements (classes).

Pratiquement parlant, vous pourriez (et la NASA ou l'ESA le voudra probablement) prouver que certains logiciels de vaisseaux spatiaux sont «sans bogue» par rapport à des spécifications précises et formalisées. Mais cela ne signifie pas que votre système se comportera toujours comme vous le souhaitez.

En termes plus simples, si votre robot de vaisseau spatial rencontre un ET et que vous ne l'avez pas spécifié, il n'y a aucun moyen de faire en sorte que votre robot se comporte comme vous le voulez vraiment ....

Lisez également les entrées du blog de J.Pitrat .

BTW, Halting problem ou le théorème de Gödel s'appliquent probablement aussi au cerveau humain, ou même à l'espèce humaine.

Cela implique-t-il que chaque programme aura au moins un comportement involontaire?

Non.

Le problème d'arrêt indique qu'il est impossible d'écrire un programme qui teste si chaque programme s'arrête dans un laps de temps fini. Cela ne signifie pas qu'il est impossible d'écrire un programme qui peut classer certains programmes comme arrêt, d'autres comme non arrêt. Ce que cela signifie, c'est qu'il existe toujours certains programmes qu'un analyseur en arrêt ne peut pas classer d'une manière ou d'une autre.

Les théorèmes d'incomplétude de Gödel ont une zone grise similaire à eux. Étant donné un système mathématique d'une complexité suffisante, il existera certaines déclarations faites dans le contexte de ce système dont la véracité ne peut être évaluée. Cela ne signifie pas que les mathématiciens doivent renoncer à l'idée de la preuve. La preuve reste la pierre angulaire des mathématiques.

Certains programmes peuvent s'avérer corrects. Ce n'est pas facile, mais cela peut être fait. C'est le but de la démonstration formelle du théorème (une partie des méthodes formelles). Les théorèmes d'incomplétude de Gödel frappent ici: il n'est pas possible de prouver que tous les programmes sont corrects. Cela ne signifie pas qu'il est tout à fait vain d'utiliser des méthodes formelles car certains programmes peuvent en effet s'avérer formellement corrects.

Remarque: les méthodes formelles excluent la possibilité qu'un rayon cosmique frappe le processeur et s'exécute launch_missiles()au lieu de a+b. Ils analysent des programmes dans le contexte d'une machine abstraite plutôt que de vraies machines qui sont sujettes à des perturbations d'un seul événement comme le rayon cosmique de Robert Harvey.

Il y a beaucoup de bonnes réponses ici, mais elles semblent toutes contourner le point critique, qui est le suivant: tous ces théorèmes ont une structure similaire et disent des choses similaires, et ce qu'ils disent n'est pas "il est impossible d'écrire probablement correctement programmes »(pour une valeur spécifique de « correcte » et « programme » qui varie en cas à l'autre ), mais ce qu'ils font dire est « il est impossible d'empêcher quelqu'un d' écrire un programme incorrect que nous ne pouvons pas prouver être incorrect »( etc).

En prenant l'exemple spécifique du problème de l'arrêt, la différence devient plus claire: il y a évidemment des programmes qui s'arrêtent de manière prouvée et d'autres programmes qui ne prouvent jamais s'arrêter. Qu'il existe une troisième classe de programmes dont le comportement ne peut pas être déterminé de toute façon n'est pas un problème si tout ce que nous voulons faire est d'écrire un programme dont l'arrêt est prouvé, car nous pouvons simplement éviter d'écrire un programme qui appartient à cette classe.

La même chose est vraie avec le théorème de Rice. Oui, pour toute propriété non triviale d'un programme, nous pouvons écrire un programme qui ne peut ni prouver que cette propriété est vraie ou fausse; nous pouvons également éviter d'écrire un tel programme car nous sommes en mesure de déterminer si un programme est prouvable.

Ma réponse sera du point de vue des affaires du monde réel et des défis auxquels chaque équipe de développement est confrontée. Ce que je vois dans cette question et dans beaucoup de réponses concerne vraiment le contrôle des défauts.

Le code peut être exempt de bogues. Prenez n'importe lequel des exemples de code "Hello World" pour n'importe quel langage de programmation, et exécutez-le sur la plate-forme à laquelle il est destiné et il fonctionnera de manière cohérente et produira les résultats souhaités. Là se termine toute théorie sur l'impossibilité d'un code sans bogue.

Les bogues potentiels apparaissent à mesure que la logique devient plus complexe. Le simple exemple Hello World n'a pas de logique et fait la même chose statique à chaque fois. Dès que vous ajoutez un comportement dynamique piloté par la logique, c'est ce qui introduit la complexité qui mène aux bogues. La logique elle-même peut être défectueuse, ou les données entrées dans la logique peuvent varier d'une manière que la logique ne gère pas.

Une application moderne dépend également des bibliothèques d'exécution, CLR, middleware, base de données, etc. qui, tout en économisant du temps de développement, sont également des couches où des bogues dans ces couches peuvent exister et ne sont pas détectés lors du développement et des tests UAT et en production.

Enfin, la chaîne d'applications / systèmes que l'application consomme des données qui alimentent sa logique sont toutes des sources de bugs potentiels soit dans leur logique, soit dans les piles logicielles que la logique chevauche, ou les systèmes en amont dont elle consomme les données.

Les développeurs ne contrôlent pas à 100% chaque pièce mobile prenant en charge la logique de leur application. En fait, nous ne contrôlons pas grand-chose. C'est pourquoi les tests unitaires sont importants, et la configuration et la gestion des changements sont des processus importants que nous ne devons pas ignorer ou être paresseux / bâclés.

En outre, des accords documentés entre votre application qui consomme des données provenant d'une source hors de votre contrôle, qui définit le format et les spécifications spécifiques pour les données transférées, ainsi que toute limite ou contrainte que votre système suppose que le système source est responsable de s'assurer que la sortie est à l'intérieur ces limites.

Dans l'application réelle du génie logiciel, vous ne pourrez pas le faire voler en expliquant à l'entreprise pourquoi les applications ne peuvent théoriquement pas être exemptes de bogues. Des discussions de cette nature entre la technologie et l'entreprise n'auront jamais lieu, sauf à la suite d'un dysfonctionnement technologique qui a affecté la capacité de l'entreprise à gagner de l'argent, à éviter de perdre de l'argent et / ou à maintenir les gens en vie. La réponse à "comment cela peut-il arriver" ne peut pas être "laissez-moi expliquer cette théorie pour que vous compreniez."

En termes de calculs massifs qui pourraient théoriquement prendre une éternité pour effectuer le calcul et obtenir un résultat, une application qui ne peut pas terminer et retourner avec un résultat - c'est un bug. Si la nature du calcul est telle qu'elle prend beaucoup de temps et demande beaucoup de calcul, vous prenez cette demande et fournissez des informations à l'utilisateur sur la façon / quand il peut récupérer le résultat, et lancez les threads parallèles pour y revenir. Si cela doit se produire plus rapidement que ce qui peut être fait sur un seul serveur et est suffisamment important pour l'entreprise, vous devez le faire évoluer sur autant de systèmes que nécessaire. C'est pourquoi le cloud est très attrayant, et la possibilité de faire tourner les nœuds pour prendre le travail et les faire tourner une fois terminé.

S'il existe la possibilité d'obtenir une demande qu'aucune quantité de puissance de calcul ne peut terminer, elle ne devrait pas traîner à l'infini avec un processus métier attendant la réponse à ce que l'entreprise pense être un problème fini.

Je ne crois pas que le code soit à 100% sans bug car le code n'est jamais vraiment fini. Vous pouvez toujours améliorer ce que vous écrivez.

La programmation est un domaine des sciences et des mathématiques, auquel cas les deux sont sans fin. La grande chose d'être un développeur est que notre travail est sans fin.

Il existe mille et une façons d'écrire une seule ligne de code. L'idée est d'écrire la version la plus optimisée de cette ligne de code, mais cela peut ne pas être exempt de bogues. Sans bogue se réfère à l'idée que votre code est incassable et que tout le code peut être cassé dans une certaine mesure ou méthode.

Le code peut-il donc être efficace? Oui.
Le code peut-il être optimisé à l'infini? Oui.
Le code peut-il être exempt de bogues? Non, vous n'avez tout simplement pas encore trouvé de moyen de le casser.
Cela étant dit, si vous vous efforcez de vous améliorer et d'améliorer vos pratiques d'écriture de code, votre code sera difficile à casser.