Ce que tu dis, c'est justement que c'est très précieux, car cela trouve jusqu'au manquement de la spec. Cela repousse le travail idiot du test systématique par une recherche d'une meilleur cohérence de spec et d'un test de haut niveau.
Personne n'a jamais dit qu'un ordinateur ferait tout le boulot à ta place.
Sinon dans les prouveurs "100% automatique", il recherche si il existe les conditions de plantage du code C, comme les "array out of bound", les division par zéro. Le but est ici de prouver que le code ne plante pas, pas qu'il correspond à la spec. C'est déjà pas mal car on ne demande rien aux codeurs "en plus".
D'une manière général, la preuve, c'est génial, sauf que cela passe rarement à l'échelle (pb numero 1) et "les gens" ne font pas confiance à un "toujours vrai" rendu par un outil, par contre, ils aiment bien qu'on trouve leur bug.
[^] # Re: mouais
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 4.
Personne n'a jamais dit qu'un ordinateur ferait tout le boulot à ta place.
Sinon dans les prouveurs "100% automatique", il recherche si il existe les conditions de plantage du code C, comme les "array out of bound", les division par zéro. Le but est ici de prouver que le code ne plante pas, pas qu'il correspond à la spec. C'est déjà pas mal car on ne demande rien aux codeurs "en plus".
D'une manière général, la preuve, c'est génial, sauf que cela passe rarement à l'échelle (pb numero 1) et "les gens" ne font pas confiance à un "toujours vrai" rendu par un outil, par contre, ils aiment bien qu'on trouve leur bug.
"La première sécurité est la liberté"