ça ne garantie pas que le programme fera ce que l'on veut (on peut très bien prouver un additionneur qui soustrait)
Moui... Je tiens à nuancer un petit peu. En fait, quand on fait de la preuve de programme, on prouve qu'un programme est correct vis-à-vis d'une spécification. Donc tout dépend de ladite spécification.
En utilisant la méthode B, on prouve par exemple que les fonctions sont toutes appelées sur leur domaine, qu'elles rendent un résultat du type attendu.
De façon plus générale, une analyse permet de prouver statiquement (c.-à-d. sans exécuter le programme) une propriété (ou un ensemble de propriétés restreint), par exemple : respect des types, pas de division par zéro, assert non violés, propriétés de sécurité (aucun SMS ne sera envoyé à l'insu de l'utilisateur d'un téléphone), etc. Voir par exemple ce que fait le logiciel Astrée [1] utilisé pour Airbus. De façon plus générale, [2] donne une bonne idée de ce qui se cache derrière les analyses statiques.
Donc, pour en revenir à l'additionneur qui soustrait, on peut prouver qu'un tel additionneur est correct vis-à-vis de la propriété « ne fait pas de fuite mémoire ». Ça ne me choque pas qu'en réalité il n'additionne pas : ce n'était pas la propriété à prouver, point.
[^] # Re: Pas exactement
Posté par dromadaire35 . En réponse au journal La sécurité informatique au 20h de TF1. Évalué à 3.
Moui... Je tiens à nuancer un petit peu. En fait, quand on fait de la preuve de programme, on prouve qu'un programme est correct vis-à-vis d'une spécification. Donc tout dépend de ladite spécification.
En utilisant la méthode B, on prouve par exemple que les fonctions sont toutes appelées sur leur domaine, qu'elles rendent un résultat du type attendu.
De façon plus générale, une analyse permet de prouver statiquement (c.-à-d. sans exécuter le programme) une propriété (ou un ensemble de propriétés restreint), par exemple : respect des types, pas de division par zéro, assert non violés, propriétés de sécurité (aucun SMS ne sera envoyé à l'insu de l'utilisateur d'un téléphone), etc. Voir par exemple ce que fait le logiciel Astrée [1] utilisé pour Airbus. De façon plus générale, [2] donne une bonne idée de ce qui se cache derrière les analyses statiques.
Donc, pour en revenir à l'additionneur qui soustrait, on peut prouver qu'un tel additionneur est correct vis-à-vis de la propriété « ne fait pas de fuite mémoire ». Ça ne me choque pas qu'en réalité il n'additionne pas : ce n'était pas la propriété à prouver, point.
[1] http://www.astree.ens.fr/(...)
[2] http://www.astree.ens.fr/IntroAbsInt.html(...)