Dureté de calcul des programmes informatiques "réels"

J'ai souvent entendu dire que vous ne pouvez pas écrire un programme pour détecter les bogues dans un navigateur Web, un traitement de texte ou un système d'exploitation, à cause du théorème de Rice: toute propriété sémantique pour un langage complet de Turing est indécidable.

Cependant, je ne sais pas dans quelle mesure cela s'applique aux programmes du monde réel comme les systèmes d'exploitation. Ces types de programmes ont-ils besoin de toute la force de l'exhaustivité de Turing? Existe-t-il des modèles de calcul plus simples (tels que PR) dans lesquels ces applications pourraient être écrites? Si oui, dans quelle mesure cela permet-il de déterminer la justesse du programme?

Vous pouvez certainement écrire des programmes qui détectent des bogues - il existe une communauté importante et active de personnes qui écrivent des programmes pour faire exactement cela. Cependant, ce que le théorème de Rice vous empêche de faire est d'écrire des capteurs de bogues à la fois solides et complets (c'est-à-dire, attraper tous les bogues d'une certaine classe sans faux positifs).

Cela dit, les restrictions naïves sur le modèle de calcul ne vous aident pas vraiment beaucoup à améliorer le caractère pratique de l'analyse de programme. La raison en est que vous pouvez obtenir des programmes qui font "presque la même chose" en tournant les boucles while

while P do 
   C

en boucles for avec une grande constante d'itération:

for i = 0 to BIGNUM do 
  if P then 
    C
  else
    break

Maintenant, ce programme n'a même pas besoin de toute la puissance de la récursivité primitive (puisque la boucle for peut être macro-développée en une énorme instruction imbriquée if-then-else), mais dans la plupart des cas pratiques, elle se comportera de la même manière qu'auparavant. Notez que cela aide à la décidabilité en théorie - le programme est total, vous pouvez donc répondre aux questions en exécutant le programme et en voyant ce qui se passe. Ce n'est pas ce que nous voulons réellement, c'est d'obtenir des réponses plus rapidement que d'exécuter le programme - la terminaison artificielle introduite n'aide pas réellement l'analyse du programme dans la pratique, car les bogues se produisent en raison d'erreurs dans la logique réelle du programme, et nous n'avons pas '' t touché à tout cela.

De plus, l'ajout de fonctions d'abstraction à un langage de programmation peut radicalement aggraver la complexité du problème d'analyse, tout en facilitant la vérification des programmes dans la pratique. Par exemple, prouver la terminaison du calcul lambda simplement tapé avec des nombres naturels nécessite une induction jusqu'à , mais en ajoutant le polymorphisme de type, vous obtenez le système F, dont la preuve de terminaison est aussi forte que la cohérence de l'arithmétique de second ordre. Pourtant, dans la pratique, les programmes écrits en F sont beaucoup plus faciles à vérifier, car les propriétés de modularité de la quantification de second ordre facilitent l'écriture de programmes structurés et de preuves d'exactitude.$\epsilon_0$

Puisque vous avez posé des questions sur l'exactitude des programmes des programmes du monde réel comme les systèmes d'exploitation, vous pourriez être intéressé par le projet seL4 ( journal , pdf , conférence ).

L'équipe NICTA a pris un micro-noyau de troisième génération de 8700 lignes de C et 600 lignes d'assembleur implémentées selon une spécification abstraite à Haskell. Ils ont fourni une preuve formelle et vérifiée par machine (dans Isabelle / HOL) que la mise en œuvre suit strictement les spécifications. Prouvant ainsi que leur programme est sans bug.

Donc, tout comme le problème d'arrêt, bien qu'il ne puisse pas être résolu en général, il peut être résolu pour certaines instances spécifiques. Dans ce cas, bien que vous ne puissiez pas prouver que le code C arbitraire est exempt de bogues, ils pourraient le faire dans le cas du micro-noyau seL4.

Les questions que vous posez sont en fait assez différentes.

Cependant, je ne sais pas dans quelle mesure cela s'applique aux programmes du monde réel comme les systèmes d'exploitation. Ces types de programmes ont-ils besoin de toute la force de l'exhaustivité de Turing?

Il faut extrêmement peu de temps pour qu'un modèle de calcul soit complet. Par exemple, différents modèles avec compteurs peuvent simuler des machines de Turing. Si vous pensez que votre logiciel nécessite plus de deux compteurs que vous pouvez manipuler arbitrairement, vous utilisez un langage complet de Turing. Bien que les entiers machine soient bornés a priori, les structures de données allouées en tas ne le sont généralement pas. Si votre logiciel a besoin de listes, d'arbres et d'autres données allouées dynamiquement, vous utilisez un langage complet de Turing.

Existe-t-il des modèles de calcul plus simples (tels que PR) dans lesquels ces applications pourraient être écrites? Si oui, dans quelle mesure cela permet-il de déterminer la justesse du programme?

Il est important de reconnaître que nous ne voulons pas vérifier les propriétés arbitraires de notre logiciel. La vérification de propriétés très spécifiques et étroites (pas de débordements de tampon, pas de déréférences de pointeur nul, pas de boucles infinies, etc.) améliore énormément la qualité et l'utilisabilité du logiciel. En théorie, de tels problèmes sont encore indécidables. En pratique, se concentrer sur des propriétés spécifiques nous permet de découvrir dans nos programmes une structure que nous pouvons souvent exploiter pour résoudre le problème.

En particulier, vous pouvez modifier votre question d'origine en

Existe-t-il une abstraction de mon logiciel que je peux analyser efficacement dans un modèle complet non Turing?

Une abstraction est un modèle qui inclut le comportement du logiciel d'origine et éventuellement de nombreux comportements supplémentaires. Il existe des modèles tels que les machines à guichet unique ou les systèmes de refoulement qui ne sont pas complets et que nous pouvons analyser. L'approche standard de la vérification de programme avec des outils automatisés consiste à construire une abstraction dans un tel modèle et à la vérifier algorithmiquement.

Il existe des applications où les gens se soucient des propriétés sophistiquées de leur matériel ou de leurs logiciels. Les entreprises de matériel informatique souhaitent que leurs puces implémentent correctement des algorithmes arithmétiques, les entreprises automobiles et avioniques souhaitent des logiciels certes corrects. Si c'est si important, il vaut mieux utiliser un être humain (formé).