Preuve de terminaison d'un algorithme

Bonsoir tout le monde,
J'ai fait un algorithme et avant de calculé sa complexité, je veux prouver que mon algorithme se termine. Le probléme, c'est que je n'ai aucune idée sur les preuves de terminaison d'un algorithme. Pourriez vous m'aider svp ?
Merci d'avance !;)

Ca dépend de ton algorithme, de sa forme, il y a des algorithmes dont il est très facile de prouver la terminaison et d'autres pour lesquels il faut connaître des maths avancés.
En gros prouver la terminaison d'un algorithme, c'est démontrer qu'il prend un nombre fini d'étape à s'exécuter quelle que soit l'entrée, dans le cas d'un algorithme récursif, ça revient à montrer qu'on revient au cas de base en un un nombre fini de récursion, pour un algorithme itératif il faut montrer que toutes les boucles terminent, etc...

--
Jedaï

parfois on reste sans preuve voir conjecture tchèque

Une technique parfois utilisée qui va fonctionner pour des algorithmes récursifs est de définir une mesure sur l'ensemble de tes paramètres à valeur dans un ensemble disposant d'une relation bien fondée. Puis de démontrer que ta mesure est strictement décroissante à chaque appel pour ta relation bien fondée

Exemple :

Code:

---

1 2 3 4 5 6 7 8 9

fonction(Naturel a, Naturel b) { Si(a=b) retourner a; Si(a<b) retourner fonction(a, b-1); Sinon retourner fonction(a-1,b); }

---

Déjà il faudrait démontrer que le typage est correct.

Ensuite, on définit la mesure m : (a,b):Nat²->max(a,b)
On utilise la relation bien fondée < dans Nat.

Ensuite, on démontre que :
Pour tout (a,b):Nat², Si(a!=b), Si a<b m(a,b-1)<m(a,b) sinon m(a-1,b)<m(a,b)

On fixe (a,b) entier naturel
Si a<b
On a m(a,b) = b
Comme a<=b-1, on a m(a,b-1) = b-1
On a bien m(a,b-1)<m(a,b)

Si b<a (car b!=a)
on a m(a,b) = a et m(a-1, b) = a-1. C'est ce qu'on voulait

Merci pour votre aide ! ;)
Mon algorithme est itératif mais il y'a beaucoup (trop ! :() de boucles. Donc is j'ai bien compris, faut juste montrer avec des formules mathématiques que mon algorithme se termine dans tous les cas (en fonction bien sur des données d'entrées) ?

Citation:

---

Donc is j'ai bien compris, faut juste montrer avec des formules mathématiques que mon algorithme se termine dans tous les cas (en fonction bien sur des données d'entrées) ?

---

Oui, si ton algo est itératif, ça revient à montrer que quelque soit les entrées tu ne rentres jamais dans une boucle infinie.

Citation:

---

Envoyé par PRomu@ld

Oui, si ton algo est itératif, ça revient à montrer que quelque soit les entrées tu ne rentres jamais dans une boucle infinie.

---

c'est trés clair ! Merci !!!!;)