Cela ressemble à des outils de preuve formelles. Dans la suite logiciel Esterel, il y avait un moyen de générer une suite d'entrée pour faire la couverture totale du code avec un outil comme prover. Ensuite, il fallait avoir écrit les conditions de validité du code (genre d'assertion). C'est l'inverse de la preuve de théorème qui ne fait que chercher un contre-exemple.
Ce genre d'approche (la génération d'entrée) est très critiqué car on semble tester un code avec lui-même. Beaucoup de gens ne font pas la différence entre la génération de pattern d'entrée (l'ATPG est pourtant un téchnique obligatoire en fabrication de puce) et la présence d'assertion ou d'oracle définit forcément à la main, car lié à la spécification de plus haut niveau.
Si vous employez un langage qui ne permet ni dépassement de capacité, ni d'allocation mémoire, ni ... boucle, c'est difficile de trouver des oracles évidents, puisque qu'il n'est pas possible d'écrire ce genre de bug. La difficulté réside ensuite dans l'écriture des assertions.
# preuve formelle ?
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Fuzzing : éprouver les entrées de vos développements. Évalué à 4.
Cela ressemble à des outils de preuve formelles. Dans la suite logiciel Esterel, il y avait un moyen de générer une suite d'entrée pour faire la couverture totale du code avec un outil comme prover. Ensuite, il fallait avoir écrit les conditions de validité du code (genre d'assertion). C'est l'inverse de la preuve de théorème qui ne fait que chercher un contre-exemple.
Ce genre d'approche (la génération d'entrée) est très critiqué car on semble tester un code avec lui-même. Beaucoup de gens ne font pas la différence entre la génération de pattern d'entrée (l'ATPG est pourtant un téchnique obligatoire en fabrication de puce) et la présence d'assertion ou d'oracle définit forcément à la main, car lié à la spécification de plus haut niveau.
Si vous employez un langage qui ne permet ni dépassement de capacité, ni d'allocation mémoire, ni ... boucle, c'est difficile de trouver des oracles évidents, puisque qu'il n'est pas possible d'écrire ce genre de bug. La difficulté réside ensuite dans l'écriture des assertions.
"La première sécurité est la liberté"