Demontrer l'exactitude d'un algorithme

Version imprimable

13/12/2008, 12h14
nathy810

Demontrer l'exactitude d'un algorithme

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!
13/12/2008, 17h41
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 .
13/12/2008, 17h46
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) ?
13/12/2008, 23h09
nathy810

bsr elmcherqui

Optimiser un algorithme !!
i.e. ameliorer veux tu dire?
merci
13/12/2008, 23h12
nathy810

bsr millie

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 ).
14/12/2008, 10h27
millie

Citation:

Envoyé par nathy810

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 ).

Citation:

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...
14/12/2008, 10h46
nathy810

merci

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
14/12/2008, 10h54
millie
Citation:

Envoyé par nathy810

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 :
Code:

1 2 3 4 5 6 7 8 fonction somme(entier n) { entier s = 0; Pour i = 1 à n { s = s + i; } retourner s; }
Dans la boucle, tu as la propriété pour les entiers (i,n,s) qui dit que : Somme des k de 1 à i = 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.
14/12/2008, 11h20
nathy810

merci encore millie mais je te pose encore une question

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
14/12/2008, 11h21
cedriku

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.
14/12/2008, 11h33
nathy810

salut cedriku

moi jai un algo ou je dois je crois trouver l invariant de boucle et meme montrer qu il est invariant de boucle
14/12/2008, 11h59
cedriku

Si t'arrives vraiment pas a voir, montre nous ton algo, dis nous ce que tu pense etre un invariant.
14/12/2008, 12h13
nathy810

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
14/12/2008, 12h25
cedriku

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 !
14/12/2008, 12h46
nathy810

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
14/12/2008, 13h17
cedriku

Citation:

Envoyé par nathy810

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

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...
14/12/2008, 13h20
nathy810

un invariant est

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
14/12/2008, 13h26
nathy810

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)
14/12/2008, 13h37
cedriku

Citation:

Envoyé par nathy810

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...).

Ca simplifiera également la preuve plutot que d'avoir deux boucles imbriquées.

Citation:

Envoyé par nathy810

est ce que je peux dire que a=r^2 est un invariant de boucle

C'est pas possible que a=r^2 soit invariant car dans la boucle a ne change jamais alors que r oui.
14/12/2008, 13h51
nathy810

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]
14/12/2008, 14h02
cedriku

Citation:

Envoyé par nathy810

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]

Non dans cet algo c'est bien a=B*Q+R l'invariant mais la ya 2 parametres qui changent dans la boucle, c'est R et Q et ils changent de sorte a garder a=B*Q+R vrai.

Alors que dans l'invariant que tu proposes a=r^2, ta un seul parametre qui change c'est r, et donc a=r^2 ne peut pas etre toujours vrai pendant la boucle (sauf si r change en -r mais ca n'est pas le cas ici) !!

Un invariant c'est juste une propriété vraie a tout moment, c'est tout, avant, pendant et apres la boucle.

Ton invariant depend donc du compteur de boucle i.
14/12/2008, 14h11
FR119492

Salut!

Citation:

Demontrer l'exactitude d'un algorithme

Démontrer un théorème ou l'exactitude d'un théorème, c'est de la logique déductive; c'est prouver rigoureusement que c'est toujours vrai. C'est ce que, sous l'influence de l'école bourbakiste, on croit devoir enseigner à nos élèves. En pratique, c'est souvent très difficile, voire même impossible. Mais il y a une autre voie: la logique inductive. Ce mode de pensée est dû à John Stuart Mill (Système de logique déductive et inductive, 1843). Pour son application aux mathématiques, je te conseille le passionnant ouvrage de György Pólya: Les Mathématiques et le raisonnement "plausible", 1958.
Jean-Marc Blanc
14/12/2008, 14h21
cedriku

Il est vrai qu'en pratique c'est impossible. Toutefois, je pense que dans son cas, c'est un exercice de devoir démontrer que son algo est correct.
14/12/2008, 14h45
nathy810

Citation:

Envoyé par cedriku

Il est vrai qu'en pratique c'est impossible. Toutefois, je pense que dans son cas, c'est un exercice de devoir démontrer que son algo est correct.

oui j ecris un algo et je dois prouver qu'il est correct.
c'est moi qui choisit de le prouver par les invariants de boucles.J'ai lu que c une methode pour demontrer qu'un algo est correct
Trouver ses invariants de boucles et demontrer qu'ils le sont
14/12/2008, 15h00
cedriku

il faut savoir aussi que la facon dont est ecrit l'algo peut influer enormement sur la preuve. Deux algo semantiquement equivalents mais syntaxiquement differents peuvent avoir des preuves differentes (une tres simple et une tres tres complique par exemple...).