Discussion :

[nathy810]

Que doit on faire exactement quand on doit montrer qu'un algo est correct?

Ce n'est pas quand même prendre un exemple, vérifier pour trouver le résultat!

[elmcherqui]

- verifier d'abord si il donne les resultats qu'on attend de lui .
- si oui voir si il est robuste c.a.d qu'il gere un maximum de cas , a toi de trouver les cas les plus tordu et extremes (a la main bien sur ) .
- et enfin optimiser si optimisation il y'a .

[millie]

Salut nathy,

Tu cherches à trouver s'il y a des chances que l'algo soit correct (tests etc.) ou à prouver formellement que ce soit correct (donc preuve avec des outils comme PVS, coq) ?

[nathy810]

Optimiser un algorithme !!
i.e. ameliorer veux tu dire?
merci

[nathy810]

merci pour ton intervention
le probleme est juste poser prouver que cette algo est correct
je ne connais ces tests dont tu parles.
Je ne suis pas une informaticienne (Pvs,coq...je ne sais pas de quoi il s 'agit ).

[millie]

merci pour ton intervention
le probleme est juste poser prouver que cette algo est correct

Je ne suis pas une informaticienne (Pvs,coq...je ne sais pas de quoi il s 'agit ).

je ne connais ces tests dont tu parles.

Je parle de tests unitaires, mais cela concerne forcement une implémentation de l'algorithme dans un langage. Donc, on teste l'implémentation sur un ensemble de valeur déterminé.
Par exemple, si j'ai une fonction qui retourne le carré d'un entier, on va tester quelques valeurs : carre(0) == 0 ?, carre(2) == 4 ? ... On teste souvent les cas normaux, les cas limites et les cas d'erreurs.


Pour la partie preuve, il y a plusieurs méthodes.
Soit on prouve l'algorithme à la main (si l'algorithme est écrit sous forme récursive, c'est plus simple, s'il est écrit sous forme impérative, c'est un peu plus compliqué).
Soit on prouve l'algorithme à l'aide de logiciel qui permettent de vérifier que ta preuve est bonne (il faut obligatoirement avoir une idée de la preuve avant de se lancer là dedans...) :
Par exemple Coq : http://coq.inria.fr/coq-fra.html
PVS : http://pvs.csl.sri.com/
A noter que ces outils permettent plus généralement de voir si une preuve est juste (n'importe quel preuve mathématiques).

C'est souvent assez délicat de comprendre comment ces outils fonctionnent et il faut pas mal d'entrainement pour savoir comment faire.

Je n'ai personnellement utilisé que PVS, j'ai tenté une fois coq, mais j'avais un peu de mal. J'ai déjà également utilisé un autre outil pour prouver des algorithmes écrit sous forme impératives, mais j'ai oublié le nom...