Discussion :

[cedriku]

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.

[FR119492]

Salut!

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

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

[nathy810]

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

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