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!
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!
- 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 .
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) ?
Je ne répondrai à aucune question technique en privé
Optimiser un algorithme !!
i.e. ameliorer veux tu dire?
merci
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 ).
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é.je ne connais ces tests dont tu parles.
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...
Je ne répondrai à aucune question technique en privé
Saurait tu ce qu'on entend par invariant de boucle?
Serait ce les variables qui dans une boucle n evolue pas au fil des calculs ou bien quoi
merci
C'est une propriété valable tout le long du déroulement d'une boucle ou d'appel récursif.
Par exemple :
Dans la boucle, tu as la propriété pour les entiers (i,n,s) qui dit que : Somme des k de 1 à i = s.
Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
8 fonction somme(entier n) { entier s = 0; Pour i = 1 à n { s = s + i; } retourner s; }
C'est un invariant de boucle.
A à la fin, tu as i=n, donc tu peux montrer que s est égal à Somme des k de 1 à n.
Je ne répondrai à aucune question technique en privé
est ce a dire que l'invariant de boucle est ce que je j'obtiens a la sortie de ma boucle.
Et s'il me faut verifier que certaines conditions sont des invariantes de boucles,je reprends juste le resultat retourner et je verifie dans ces conditions?
Ce que je fais est purement mathematique mais l informatique que je retrouve dedans me perds
je ne suis pas calée en info hein!
merci
Salut,
a noter que ton invariant de boucle est une propriété qui doit etre vraie à 4 endroits :
- Avant de rentrer dans la boucle
- Au début de la boucle
- A la fin de la boucle (c'est-a-dire juste avant d'effectuer le test de sortie de boucle)
- Après la boucle
La difficulté c'est donc de trouver l'invariant surtout si la boucle est complexe.
moi jai un algo ou je dois je crois trouver l invariant de boucle et meme montrer qu il est invariant de boucle
Si t'arrives vraiment pas a voir, montre nous ton algo, dis nous ce que tu pense etre un invariant.
cet algo je l'ai redigé suite a bcp d'autres questions precedentes
en supposant donc que je l'ai trouvé
c:=b^t mod (p);
r=a^(t+1)/2 mod p;
Pour i=1 à s-1 faire
d=[(r^2)a^-1]^2^(s-i-1);
tant que d<>1 mod p faire
r:=r*c mod(p);
c:=c^2 mod p;
fintantq
finpour
retourner(r,-r)
l'invariant de boucle est il r:=r*c.
en fait je ne sais pas encore vraiment mais je soumets deja mon algo
je reecris ds un instant si j ai kelke chose de nouveau
Bon, dejà pour etre clair, est ce que c'est :
r=(a^(t+1))/2 mod p
ou bien
r=a^((t+1)/2) mod p
pour savoir si le 2 est dans la puissance ou c'est le tout sur 2 ?
Ensuite ou se termine ta boucle Pour ? (je suppose juste avant le tant que mais suis pas sur)
Ensuite il y a un probleme pour ta boucle Tant Que :
Tu dis tant que d<>1... or d ne change jamais de valeur dans la boucle, donc si tu y rentre la premiere fois, tu n'en sortiras jamais (d sera toujours different de 1) -> boucle infinie. Donc ceci me fait penser que finalement la boucle Tant Que est imbriqué dans la boucle Pour ???
Indique bien les fin de tes boucle avec FinPour ou FinTantQue par exemple car sinon on ne sait pas si elle sont imbriquées ou pas...
Autre chose, donnes les spécification de ton algo, c'est-à-dire, les données en entrées (je suppose que c'est a,b,p, s et t), et le resultat que ca doit renvoyer !
c est ceci pour etre bien precise
r=[a^((t+1)/2)]mod p
le 2 est dans la puissance
Ensuite ou se termine ta boucle Pour ? (je suppose juste avant le tant que mais suis pas sur)
Non tant que est dans ma boucle pour
en fait j ai mis finpour en dessous vois tu?
Ensuite il y a un probleme pour ta boucle Tant Que :
Tu dis tant que d<>1... or d ne change jamais de valeur dans la boucle, donc si tu y rentre la premiere fois, tu n'en sortiras jamais (d sera toujours different de 1) -> boucle infinie. Donc ceci me fait penser que finalement la boucle Tant Que est imbriqué dans la boucle Pour ???
elle est imbriquée comme tu dis
je teste si d est 1 je n entre pas dans tantque et sinon d evolue avec le i
Indique bien les fin de tes boucle avec FinPour ou FinTantQue par exemple car sinon on ne sait pas si elle sont imbriquées ou pas...
tu as eu mon message non achevé
je reeditais encore
les resultats d'est r et -r
en entrees je prends juste p et a
les autres variables sont juste calculées
bien sur que je les declare
(t,s,d,c,b)
j avais a une fiche precedente ecrit une fonction qui retrouve t et s avec un p premier donné.
bon je crois que c est un peu plus clair
Oui mais imagine tu rentre dans la boucle Tant Que, dans cette boucle, seuls r et c sont modifiés donc le test d<>1 sera toujours vrai et tu n'en sortira jamais !!! Le seul endroit ou d est modifié c'est en dehors de la boucle Tant Que...Envoyé par nathy810
je veux trouver les racines de a mod p
est ce que je peux dire que a=r^2 est un invariant de boucle
je crois que ce doit etre verifier a chaque fois dans mon algo
quitte a le verifier je vais chercher a montrer
je me demande donc now si un seul suffit?
merci
je vais modifier un truc dans mon algo encore
c:=b^t mod (p);
r=a^(t+1)/2 mod p;
Pour i=1 à s-1 faire
d=[(r^2)a^-1]^2^(s-i-1);
si d<>1 mod p faire
r:=r*c mod(p);
c:=c^2 mod p;
finsi
finpour
retourner(r,-r)
Bon deja, le fait de mettre un Si plutot que Tant Que, c'est bien mieux (je sais pas si c'est juste par rapport au calcul que tu veux faire mais au moins t'as plus de boucle infinie...).Envoyé par nathy810
Ca simplifiera également la preuve plutot que d'avoir deux boucles imbriquées.
C'est pas possible que a=r^2 soit invariant car dans la boucle a ne change jamais alors que r oui.
mais la je crois que je n ai pas bien pigé ce que c est qu un invariant.
je viens de lire un exemple
l'algo d euclide
ils disent que a=B*Q+R est un invariant de boucle alors qu ici aussi a ne change pas dans la boucle tantque
B := b;
R := a;
Q := 0;
Tant que R ≥ B faire
R := R − B ;
Q := Q + 1 ;
fintq ;
je dois encore bien cerner la notion "invariant de boucle"
ou alors tu aimerais que je dise r^2=a
ca va?[/COLOR]
Vous avez un bloqueur de publicités installé.
Le Club Developpez.com n'affiche que des publicités IT, discrètes et non intrusives.
Afin que nous puissions continuer à vous fournir gratuitement du contenu de qualité, merci de nous soutenir en désactivant votre bloqueur de publicités sur Developpez.com.
Partager