Bonsoir.

Prenons un exemple : l'algorithme d'Euclide. Vas-y.

Bonsoir GBZM,

Merci pour ta réponse.
En fait, j'ai l'impression que la « formule que l'on programme »(je ne sais pas comment l'exprimer autrement) donne « automatiquement » un invariant de boucle.
J'essaie de répondre à ton exo(avec a>b>0)
Fonction Pgcd(a,b):
r0 prend la valeur a
r1 prend la valeur b
Tq r1> 0 faire:
r0 prend la valeur r1
r1 prend la valeur r0%r1
Fintq
Retourner r0

Benh disons que le truc qui reste invariant c'est  pgcd(r0,r1), mais c'est parce que mon algorithme est construit sur cette idée. Donc cela veut dire que mon invariant de boucle je l'ai en fait dès l'instant où je conçois mon programme?

Ton algorithme est mal écrit : tu affectes à r0 la valeur de r1, puis tu calcules r0%r1. Ça va te donner 0 illico presto !
Plutôt : r0,r1 = r1,r0%r1

Ceci étant corrigé, je dirais plutôt que l'invariant de boucle est l'ensemble des diviseurs communs de r0 et r1 (on ne sait pas encore qu'il y a un pgcd).
On a un invariant de boucle et la terminaison de l'algorithme vu que la suite des entiers naturels r1 est strictement décroissante. Comme ça se termine avec un couple r0,r1=0, on a que l'ensemble des diviseurs communs de a et b est égal à l'ensemble des diviseurs communs de r0 et de 0, c.-à-d. l'ensemble des diviseurs de r0. Ceci montre que r0 est pgcd de a et b et établit donc l'existence d'un pgcd.

Oui évidemment pour l'algorithme, je l'ai écrit à la hâte .
Oui aussi pour l'invariant, c'est très clair.
Mais alors, quelle est la réponse à ma question, à savoir l'existence ou non d'une méthode systématique? Merci beaucoup pour ton aide précieuse!!

Je ne vois pas d'autre méthode que la compréhension fine de ce que fait l'algorithme.