J'ai donné les deux définitions, qui sont clairement différentes. Pour ceux qui dorment au fond [,qui écrivent sans avoir lu et qui moinssent à la vue du nom de l'auteur], voici un exemple très simple. Le bug de l'instruction FDIV du Pentium 1, pourtant réalisée par un algorithme pour lequel il existe une preuve de correction, était dû à l'absence de certaines entrées dans une table de valeurs précalculées.
Pour la preuve, ceci n'existe pas. Lorsqu'il y a une table de valeurs précalculées dans une preuve, cette table est une constante. Vérifier que toutes les valeurs y sont n'a guère de sens puisque ça revient à écrire l'assertion selon laquelle une constante est égale à elle-même.
Du point de vue des tests (après coup, bien sûr, c'est toujours plus facile), il aurait fallu un test par entrée de la table. Comme le test porte sur la table produite et non sa spécification, ce n'est plus équivalent à une opération nulle.
C'est un exemple-jouet, bien sûr, mais c'est déjà suffisant pour montrer que la preuve de programmes et le test sont deux disciplines différentes qui s'intéressent à deux choses différentes. Il n'y a clairement pas d'inclusion de l'une dans l'autre. Après, on peut remarquer tant qu'on veut qu'elles utilisent des méthodes similaires : on utilise des automates aussi en traitement automatique des langues, pourtant je n'ai entendu personne déclarer que le TAL est inclus dans la preuve de programmes. Pas encore, du moins.
[^] # Re: Se passer des tests ...
Posté par ɹǝıʌıʃO . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 3.
Pour la preuve, ceci n'existe pas. Lorsqu'il y a une table de valeurs précalculées dans une preuve, cette table est une constante. Vérifier que toutes les valeurs y sont n'a guère de sens puisque ça revient à écrire l'assertion selon laquelle une constante est égale à elle-même.
Du point de vue des tests (après coup, bien sûr, c'est toujours plus facile), il aurait fallu un test par entrée de la table. Comme le test porte sur la table produite et non sa spécification, ce n'est plus équivalent à une opération nulle.
C'est un exemple-jouet, bien sûr, mais c'est déjà suffisant pour montrer que la preuve de programmes et le test sont deux disciplines différentes qui s'intéressent à deux choses différentes. Il n'y a clairement pas d'inclusion de l'une dans l'autre. Après, on peut remarquer tant qu'on veut qu'elles utilisent des méthodes similaires : on utilise des automates aussi en traitement automatique des langues, pourtant je n'ai entendu personne déclarer que le TAL est inclus dans la preuve de programmes. Pas encore, du moins.