Les preuves d'exactitude du code seront-elles un jour généralisées? [fermé]

14

Tous les programmes sauf les plus triviaux sont remplis de bogues et donc tout ce qui promet de les supprimer est extrêmement séduisant. Pour le moment, les preuves d'exactitude sont du code sont extrêmement ésotériques, principalement en raison de la difficulté à apprendre cela et de l'effort supplémentaire qu'il faut pour prouver qu'un programme est correct. Pensez-vous que la preuve du code prendra son envol?

programming-practices Casebash
la source

Réponses:

8

Pas vraiment dans ce sens, mais la programmation fonctionnelle pure est bonne dans ce domaine. Si vous utilisez Haskell, il est probable que votre programme soit correct si le code compile. Sauf pour IO, un bon système de type est une bonne aide.

La programmation pour contracter peut également être utile. Voir les contrats de code Microsoft

Jonas
la source
6
Désolé - je n'ai pas fait beaucoup de "vrai monde" Haskell, mais j'ai fait assez d'exercices de tutoriel pour plusieurs vies. Ce n'est pas parce qu'il compile qu'il est susceptible de fonctionner. Comparé par exemple à Ada (choisi parce que c'est un langage impératif strictement typé), je dirais que Haskell est un peu plus facile, mais surtout parce qu'il est plus concis (complexité cyclomatique plus faible). Lorsque vous traitez avec la monade IO, il y a des ennuis qui peuvent rendre Haskell plus difficile à corriger - c'est juste assez différent du style impératif qu'il y a des choses qu'il ne peut pas faire aussi naturellement.
Steve314
Sur "ne peut pas faire aussi naturellement", considérez une boucle "while". Oui, vous pouvez rouler le vôtre - mais la condition while doit être dans la monade car elle doit réagir aux effets secondaires du corps de la boucle. Non seulement cela signifie que vous avez été autorisé à provoquer des effets secondaires dans la condition while, mais il est également difficile d'utiliser cette boucle while. Résultat final - il est généralement plus facile d'utiliser la récursivité même dans le code de monade IO - et cela signifie que vous devez structurer les choses d'une manière particulière.
Steve314
14

Tous les programmes sauf les plus triviaux

ne peut être entièrement vérifié pour être correct avec un effort raisonnable. Pour toute preuve formelle d'exactitude, vous avez besoin d'au moins une spécification formelle, et cette spécification doit être complète et correcte. Ce n'est généralement rien que vous puissiez facilement créer pour la plupart des programmes du monde réel. Par exemple, essayez d'écrire une telle spécification pour quelque chose comme l'interface utilisateur de ce site de discussion, et vous savez ce que je veux dire.

Ici, j'ai trouvé un bel article sur le sujet:

http://www.encyclopedia.com/doc/1O11-programcorrectnessproof.html

Doc Brown
la source
Bon - pour tout projet de programmation, il y a une transition d'une description informelle du problème à une description formelle (généralement, aujourd'hui, sous la forme d'un programme), et cela ne disparaît pas.
David Thornley
astree.ens.fr Voir les applications industrielles d'Astrée ici
zw324
@ZiyaoWei: ces outils sont utiles, mais ils ne trouvent que quelques erreurs formelles, pas plus. Si un programme d'une ligne comme printf("1")est correct ou non (par exemple, parce que l'exigence était "d'imprimer un nombre aléatoire également distribué de 1 à 6") ne peut pas être décidé par un tel analyseur statique.
Doc Brown
10

Le problème avec les preuves formelles est qu'elles ne font que reculer le problème d'une étape.

Dire qu'un programme est correct équivaut à dire qu'un programme fait ce qu'il doit faire. Comment définissez-vous ce que le programme doit faire? Vous le spécifiez. Et comment définissez-vous ce que le programme doit faire dans les cas marginaux que la spécification ne couvre pas? Eh bien, alors vous devez rendre la spécification plus détaillée.

Supposons donc que vos spécifications deviennent finalement suffisamment détaillées pour décrire le comportement correct de chaque aspect de l'ensemble du programme. Vous avez maintenant besoin d'un moyen de faire comprendre vos outils de preuve. Vous devez donc traduire la spécification dans une sorte de langage formel que l'outil de preuve peut comprendre ... hé, attendez une minute!

Mason Wheeler
la source
2
Aussi .. "Méfiez-vous des bogues dans le code ci-dessus; je l'ai seulement prouvé correct, pas essayé." - Donald Knuth
Brendan
8

La vérification formelle a parcouru un long chemin, mais généralement les outils de l'industrie / largement utilisés sont à la traîne des dernières recherches. Voici quelques efforts récents dans cette direction:

Spec # http://research.microsoft.com/en-us/projects/specsharp/ Il s'agit d'une extension de C # qui prend en charge les contrats de code (conditions pré / post et invariants) et peut utiliser ces contrats pour effectuer différents types d'analyse statique .

Des projets similaires à celui-ci existent pour d'autres langages, tels que JML pour java, et Eiffel a à peu près cela intégré.

Pour aller encore plus loin, des projets comme le slam and blast peuvent être utilisés pour vérifier certaines propriétés comportementales avec une annotation / intervention minimale du programmeur, mais ne peuvent toujours pas traiter la généralité complète des langages modernes (des choses comme l'arithmétique du débordement d'entier / du pointeur ne sont pas modélisées).

Je crois que nous verrons beaucoup plus de ces techniques utilisées dans la pratique à l'avenir. Le principal obstacle est que les invariants de programme sont difficiles à déduire sans annotations manuelles, et les programmeurs ne sont généralement pas disposés à fournir ces annotations car cela est trop fastidieux / prend trop de temps.

Lucina
la source
4

Non, sauf si une méthode de vérification automatique du code sans travail de développeur approfondi se pose.

Fishtoaster
la source
Considérez l'argument économique: il est peut-être préférable pour les développeurs de "perdre" du temps avec des preuves d'exactitude que de perdre de l'argent à cause d'erreurs logicielles.
Andres F.
Je suis d'accord avec fishtoaster, à moins que cela ne consomme beaucoup moins de ressources, beaucoup de logiciels commerciaux réguliers n'auront tout simplement pas le coût / avantage pour supporter ce niveau d'exactitude. Dans une application LOB destinée à un public captif, l'avantage le plus rentable pour un rapport de bogue est parfois d'ajouter une ligne aux documents qui dit "ne fais pas ça"
Bill
3

Certains outils de méthodes formelles (comme par exemple Frama-C pour les logiciels C embarqués critiques) peuvent être considérés comme (en quelque sorte) fournissant, ou du moins vérifiant, une preuve (d'exactitude) d'un logiciel donné. (Frama-C vérifie qu'un programme obéit à sa spécification formalisée, dans un certain sens, et respecte les invariants explicitement annotés dans le programme).

Dans certains secteurs, de telles méthodes formelles sont possibles, par exemple comme le DO-178C pour les logiciels critiques des aéronefs civils. Dans certains cas, de telles approches sont donc possibles et utiles.

Bien sûr, développer des logiciels moins bogués est très coûteux. Mais l'approche de méthode formelle a du sens pour une sorte de logiciel. Si vous êtes pessimiste, vous pourriez penser que le bogue est déplacé du code vers sa spécification formelle (qui peut avoir quelques "bogues", car formaliser le comportement prévu d'un logiciel est difficile et sujet aux erreurs).

Basile Starynkevitch
la source
3

Je suis tombé sur cette question, et je pense que ce lien pourrait être intéressant:

Applications industrielles d'Astrée

Prouver l'absence de RTE dans un système utilisé par Airbus avec plus de 130 000 lignes de code en 2003 ne semble pas être mauvais, et je me demande s'il y aura quelqu'un pour dire que ce n'est pas le monde réel.

zw324
la source
2

Non. Le proverbe commun est: "En théorie, la théorie et la pratique sont les mêmes. En pratique, non."

Un exemple très simple: Typos.

En fait, l'exécution du code via des tests unitaires trouve ces choses presque immédiatement, et un ensemble cohérent de tests annulera le besoin de preuves formelles. Tous les cas d'utilisation - bons, mauvais, erreurs et cas limites - doivent être énumérés dans les tests unitaires, qui se révèlent être une meilleure preuve que le code est correct que n'importe quelle preuve distincte du code.

Surtout si les exigences changent ou si l'algorithme est mis à jour pour corriger un bogue - la preuve formelle est plus susceptible de devenir obsolète, comme les commentaires de code l'obtiennent souvent.

Izkata
la source
3
Faux. Aucun test unitaire ne pourra jamais couvrir l'ensemble des paramètres possibles. Imaginez "tester de manière unitaire" un compilateur de cette façon, en vous assurant qu'aucun changement de passe ne sémantique.
SK-logic
3
les tests unitaires ne sont pas le Saint Graal ...
Ryathal
1
@Winston Ewert, il existe des compilateurs vérifiés (et bien d'autres assembleurs vérifiés). Et le matériel est officiellement vérifié beaucoup plus souvent que le logiciel. Voir ici: gallium.inria.fr/~xleroy/publi/compiler-certif.pdf
SK-logic
1
@ SK-logic, oui, il existe des compilateurs de jouets qui ont fait leurs preuves à des fins académiques. Mais qu'en est-il des compilateurs que les gens utilisent réellement? Je soupçonne que la plupart des compilateurs sont vérifiés à l'aide de diverses formes de tests automatisés et presque aucune preuve correcte formelle n'est effectuée.
Winston Ewert
1
@Winston Ewert, les preuves d'exactitude sont pratiques et largement utilisées dans la vie réelle. Ce qui n'est pas très pratique, c'est la plupart des langues traditionnelles modernes. J'espère qu'ils disparaîtront tous, donc la valeur des preuves d'exactitude augmentera à l'avenir.
SK-logic
1

Je pense que les limites imposées aux preuves de correction en raison du problème d'arrêt pourraient être le plus grand obstacle à la généralisation des preuves de correction.

Paddyslacker
la source
8
Le problème d'arrêt indique que nous ne pouvons pas déterminer si un programme arbitraire s'arrête. Ces programmes peuvent faire des choses étranges, comme tester chaque entier pour voir s'il s'agit d'un nombre premier de Mersenne. Nous ne faisons pas cela dans les programmes normaux!
Casebash
1
@Casebash, la question est de savoir s'il existe un sous-ensemble utile de programmes pour lesquels le problème d'arrêt peut être résolu. Ce n'est en aucun cas clair dans les deux cas. Autrement dit, pouvons-nous restreindre nos programmes afin que nous ne puissions pas faire des choses comme tester chaque entier sans ruiner notre capacité à effectuer des tâches utiles?
Winston Ewert
1

Il est déjà utilisé par tout le monde. Chaque fois que vous utilisez la vérification de type de votre langage de programmation, vous faites essentiellement une preuve mathématique de l'exactitude de votre programme. Cela fonctionne déjà très bien - il vous suffit de choisir des types corrects pour chaque fonction et structure de données que vous utilisez. Plus le type est précis, meilleure sera la vérification. Les types existants disponibles dans les langages de programmation disposent déjà d'outils suffisamment puissants pour décrire presque tous les comportements possibles. Cela fonctionne dans toutes les langues disponibles. C ++ et les langages statiques font juste les vérifications au moment de la compilation, tandis que les langages plus dynamiques comme python le font lorsque le programme est exécuté. Le chèque existe toujours dans toutes ces langues. (par exemple, c ++ prend déjà en charge la vérification des effets secondaires de la même manière que haskell,

tp1
la source
Avec le peu d'effets secondaires en C ++, faites-vous référence à l'exactitude des const?
Winston Ewert
oui, fonction membre const + const. Si toutes vos fonctions membres sont const, toutes les données des objets ne sont pas modifiables.
tp1
Ils sont toujours modifiables si vous utilisez mutableou const_cast. Je vois certainement le lien que vous y établissez, mais la saveur de deux approches me semble plutôt différente.
Winston Ewert
Eh bien, c'est pourquoi vous devez choisir de l'utiliser - il existe toujours des moyens de le contourner. Mais l'important est de savoir comment faire pour que les compilateurs vérifient les problèmes dans la région.
tp1