Posté par gasche .
En réponse à la dépêche OCaml 4.03.
Évalué à 4.
Dernière modification le 05 mai 2016 à 03:37.
Mais invoquer Rice pour la preuve de programme ne me semble pas à côté de la plaque...
Le théorème de Rice dit que pour une propriété non-triviale Pfixée sur les machines de Turing (exprimée en terme du langage reconnu par la machine), la question de savoir si une machine quelconque vérifie P est indécidable.
Le problème que nous sommes en train de discuter est de savoir si un programme correspond à sa spécification, elle-même décrite dans un langage fixé. En particulier, on ne regarde pas une propriété fixée sur tous les programmes, mais une propriété différente pour chaque programme. (On pourrait considérer la paire (programme, spécification) comme le programme (un programme annoté), mais la propriété que l'on veut vérifiée n'est pas exprimable en terme du langage reconnu par le programme annoté, ou plus généralement du comportement observable du programme annoté.)
Une autre façon de voir que ce théorème ne s'applique pas du tout à ce problème est la suivante: dans les langages avec un système de type correct, le système de typage garantit l'absence de tout une classe d'erreurs pendant l'exécution (typiquement les accès mémoire incorrects, segfault et compagnie): "well-typed programs do not get stuck". Suivant ton raisonnement, le théorème de Rice suggèrerait que c'est impossible—le typeur décide en un temps fini d'accepter ou non le programme, et pourtant il garantit une propriété non-triviale. Mais d'une part on ne part pas de machines de Turing arbitraires, on part de programmes écrits dans un langage conçu pour le typage qui contient des constructions qui guident le typeur, et d'autre part on ne demande pas à décider l'absence de cette classe d'erreur, on se contente d'une sous-approximation correcte (il y a des programmes qui ne sont pas erronés mais qui sont rejetés par le typeur).
Le fait d'être bien typé peut s'étendre à une notion plus générale de "vérifier une spécification", puisqu'on peut exprimer une spécification comme un type dans certains systèmes—ou choisir de garder ces deux notions séparées, mais la même explication marche pour les spécifications. Bien sûr, plus le système de typage est simple, plus le typeur est facile à écrire—aujourd'hui les outils utilisés pour vérifier les spécifications demandent encore trop d'effort par rapport à ce qu'on voudrait. Mais c'est une question d'interface utilisateur, ça ne correspond pas à une impossibilité théorique venant du théorème de Rice. (Si on veut invoquer un théorème pour justifier la difficulté, il vaudrait mieux partir sur le fait que les preuves sans coupure peuvent être exponentiellement plus larges que des preuves avec, qui explique bien les limitations pratiques d'une partie des approches de démonstration automatique.)
Alors certes on pourrait imaginer un outil qui nous aiderai tellement que la partie à faire à la main serait super facile, mais un tel outil n'existe pas.
Il n'existe pas aujourd'hui (enfin Why3 ou Dafny vont déjà assez loin dans cette direction), mais on y travaille—et le but n'est pas "super facile", mais "au final comparé au temps qu'on aurait passé à débugger, ou aux problèmes causés par les bugs pour ce programme, on y gagne".
[^] # Re: Et pendant ce temps, CamlLight poursuite sa route...
Posté par gasche . En réponse à la dépêche OCaml 4.03. Évalué à 4. Dernière modification le 05 mai 2016 à 03:37.
Le théorème de Rice dit que pour une propriété non-triviale
Pfixée sur les machines de Turing (exprimée en terme du langage reconnu par la machine), la question de savoir si une machine quelconque vérifiePest indécidable.Le problème que nous sommes en train de discuter est de savoir si un programme correspond à sa spécification, elle-même décrite dans un langage fixé. En particulier, on ne regarde pas une propriété fixée sur tous les programmes, mais une propriété différente pour chaque programme. (On pourrait considérer la paire (programme, spécification) comme le programme (un programme annoté), mais la propriété que l'on veut vérifiée n'est pas exprimable en terme du langage reconnu par le programme annoté, ou plus généralement du comportement observable du programme annoté.)
Une autre façon de voir que ce théorème ne s'applique pas du tout à ce problème est la suivante: dans les langages avec un système de type correct, le système de typage garantit l'absence de tout une classe d'erreurs pendant l'exécution (typiquement les accès mémoire incorrects, segfault et compagnie): "well-typed programs do not get stuck". Suivant ton raisonnement, le théorème de Rice suggèrerait que c'est impossible—le typeur décide en un temps fini d'accepter ou non le programme, et pourtant il garantit une propriété non-triviale. Mais d'une part on ne part pas de machines de Turing arbitraires, on part de programmes écrits dans un langage conçu pour le typage qui contient des constructions qui guident le typeur, et d'autre part on ne demande pas à décider l'absence de cette classe d'erreur, on se contente d'une sous-approximation correcte (il y a des programmes qui ne sont pas erronés mais qui sont rejetés par le typeur).
Le fait d'être bien typé peut s'étendre à une notion plus générale de "vérifier une spécification", puisqu'on peut exprimer une spécification comme un type dans certains systèmes—ou choisir de garder ces deux notions séparées, mais la même explication marche pour les spécifications. Bien sûr, plus le système de typage est simple, plus le typeur est facile à écrire—aujourd'hui les outils utilisés pour vérifier les spécifications demandent encore trop d'effort par rapport à ce qu'on voudrait. Mais c'est une question d'interface utilisateur, ça ne correspond pas à une impossibilité théorique venant du théorème de Rice. (Si on veut invoquer un théorème pour justifier la difficulté, il vaudrait mieux partir sur le fait que les preuves sans coupure peuvent être exponentiellement plus larges que des preuves avec, qui explique bien les limitations pratiques d'une partie des approches de démonstration automatique.)
Il n'existe pas aujourd'hui (enfin Why3 ou Dafny vont déjà assez loin dans cette direction), mais on y travaille—et le but n'est pas "super facile", mais "au final comparé au temps qu'on aurait passé à débugger, ou aux problèmes causés par les bugs pour ce programme, on y gagne".