"Une preuve fausse n'a pas beaucoup d'intérêt."
Si, on sait qu'on peut foutre le programme à la poubelle, ou au moins le corriger pour le rendre valide.
Je dirais même plus, c'est le plus utile !
Il est souvent beaucoup plus facile de trouver un contre exemple à un moteur de preuve que de d'assurer que l'ensemble des possibles est couvert.
De plus, d'un point de vue psychologie d'un programmeur, on comprend mieux une erreur avec le contre exemple qui force la correction. Si le programme rend "prouvé", il y a beaucoup de monde qui n'y croira pas.
Cela signifie qu'il vaut mieux chercher "large" que tenter de prouver complètement des bouts minuscules.
Les 2 téchniques que je connais c'est la résolution d'équation logiques SAT et les BDD (parcoure de tous les états possible).
C'est le moyen de faire une preuve "définitive" mais qui finit toujours par exploser en temps. Dans ce cas, des méthodes basé sur un montecarlo peut tout à fait fonctionner pour trouver un contre exemple.
[^] # Re: C'est trop compliqué !
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Des langages de haut niveau. Évalué à 2.
Si, on sait qu'on peut foutre le programme à la poubelle, ou au moins le corriger pour le rendre valide.
Je dirais même plus, c'est le plus utile !
Il est souvent beaucoup plus facile de trouver un contre exemple à un moteur de preuve que de d'assurer que l'ensemble des possibles est couvert.
De plus, d'un point de vue psychologie d'un programmeur, on comprend mieux une erreur avec le contre exemple qui force la correction. Si le programme rend "prouvé", il y a beaucoup de monde qui n'y croira pas.
Cela signifie qu'il vaut mieux chercher "large" que tenter de prouver complètement des bouts minuscules.
Les 2 téchniques que je connais c'est la résolution d'équation logiques SAT et les BDD (parcoure de tous les états possible).
C'est le moyen de faire une preuve "définitive" mais qui finit toujours par exploser en temps. Dans ce cas, des méthodes basé sur un montecarlo peut tout à fait fonctionner pour trouver un contre exemple.
"La première sécurité est la liberté"