En général, tu fais un test pour couvrir un point de spécification. Donc, tu trouves à la main des vecteurs d'entrée, tu évalue ce que doivent être tes sorties et tu compares avec la sortie de ton code.
Dans la preuve formel, tu ajoutes une assertion qui correspond à un point de spécification. La vérification formel balaye toutes les possibilités d'entrée à la recherche d'un contre exemple.
Dans le cas du test, tu es limité par les vecteurs d'entrée que tu trouves à la main alors qu'avec un moteur de preuve, tu as l'exhaustivité.
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 1.
Dans la preuve formel, tu ajoutes une assertion qui correspond à un point de spécification. La vérification formel balaye toutes les possibilités d'entrée à la recherche d'un contre exemple.
Dans le cas du test, tu es limité par les vecteurs d'entrée que tu trouves à la main alors qu'avec un moteur de preuve, tu as l'exhaustivité.
"La première sécurité est la liberté"