Discussion :

[Pouknouki]

Bonjour à tous
Je suis en prépa maths option informatique et on nous apprend à prouver qu'un algorithme termine et est correct, en utilisant notamment des invariants de boucle. J'ai quelques questions concernant ceux-ci. Soit l'algorithme suivant :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
x ← 1
y ← 1
tant que x ≤ y faire
afficher (x)
x → x ∗ 2
y → y+10
fin tant que

On me demande ce qu'il affichera et de proposer un invariant de boucle. Naturellement, j'ai donné "après n passages, 2^n <= 1 + 10n". Est ce que c'est ce qu'on attend e moi ? Ca peut paraître bête comme question mais je vois pas vraiment quoi mettre d'autre, et non plus en quoi ça peut nous donner ce que l'algorithme affichera (en faisant une résolution sur WolframAlpha, je trouve que le dernier n sera 5, donc ça affichera 1, 2, 4, 8, 16, 32).
Ensuite, pour un programme aussi simple que

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
tant que 2^n*b ≤ a faire
n → n+1
fin tant que

Que donner comme invariant de boucle ? "2^n*b ≤ a" ?
Merci d'avance

[Flodelarab]

Bonjour

Je connaissais pas cette notion "d'invariant de boucle" et je ne suis pas sûr d'avoir totalement saisi l'intérêt. Mais cela force à se demander si la boucle se termine.

Dans le premier cas, on est moins sûr que la boucle se termine avec "x ≤ y", qu'avec "2^n <= 1 + 10n".

Dans le second cas, si tu veux faire savant, tu peux écrire:

[dourouc05]

Par définition, l'invariant est une propriété valide avant et après chaque itération de la boucle, y compris avant son exécution et après la dernière itération. (Cf. https://fr.wikipedia.org/wiki/Invariant_de_boucle.) Or, si la boucle se termine, tu as forcément x > y, soit 2^n > 1 + 10n — sa négation ne peut donc pas être ton invariant.

Ne pourrais-tu pas dire que x = 2^n et y = 1 + 10 n, où n est le nombre d'itérations effectuées, est ton invariant ? Puisque l'entier n augmente d'itération en itération, que la propriété x <= y est vérifiée pour n = 4 mais pas pour n = 5, ton algorithme doit se terminer. Enfin, je pense, sans certitude aucune…

[Pouknouki]

Ah oui tu as raison !
Bah du coup le coup du x = 2^n et y = 1+10n me paraît bien mais je sais pas parce que ça ne prouve en rien que ça termine (pour prouver que ça termine le prof a dit qu'il fallait trouver une valeur qui diminuait strictement à chaque passage mais je sais plus comment il a appelé ça). Donc ça permettrait de savoir ce que ça renvoie ? Ce qu'il y a c'est que pour savoir ce que ça renvoie, il faut connaître le n, ce qui se fait en résolvant 2^n <= 1 + 10n soit -1≤2^(log_2((10n)))-2^n mais résoudre ça je ne sais pas le faire à part comme ça...

[pseudocode]

Bonsoir,

Je trouve cela plus simple si on aborde ce problème avec les états (cf. machine de Turing).

Une boucle consiste a partir d'un état initial, de faire des itérations qui modifient l'état, pour arriver dans un état final:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
 
E0 /* etat initial */
TANTQUE(Condition=true) FAIRE
     Ei+1 = f(Ei) /* modification de l'état */
FIN TANTQUE
En /* etat final */

Un invariant de boucle est une propriété qui est vraie quel que soit l'état (initial, intermédiaires, final)

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
E0 /* etat initial */
ASSERT(Invariant(E0) = true)
TANTQUE (Condition=true) FAIRE
     Ei+1 = f(Ei) /* modification de l'état */
     ASSERT(Invariant(Ei+1) = true)
FIN TANTQUE
En /* etat final */
ASSERT(Invariant(En) = true)

Un variant de boucle est une valeur entière qui doit:
1. toujours être positive.
2. décroitre à chaque itération.
Ces 2 conditions prouvent forcément que la boucle s'arrête, sinon le variant deviendrait négatif/nul.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
E0 /* etat initial */
ASSERT(Variant(E) >= 0 )
TANTQUE (Condition=true) FAIRE
     Ei+1 = f(Ei) /* modification de l'état */
     ASSERT(0 < Variant(Ei+1) < Variant(Ei))
FIN TANTQUE
En /* etat final */

[Pouknouki]

Merci pour cette dernière réponse qui ajoute plus de précision. En gros, si je comprends bien, l'invariant sert à démontrer la correction et le variant la terminaison, c'est ça ?
Du coup, pour mon exercice avec le 2^n et le 1+10n, je peux utiliser comme invariant de boucle "x = 2^n et y = 1+10n" ? Il est toujours valable celui-là. On ne me demande pas de variant de boucle dans l'exercice, mais est ce que je pourrais par exemple utiliser la différence entre x et y ? Logiquement elle décroît strictement puisqu'on sort de la boucle...
Concernant le programme suivant :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
tant que 2^n*b ≤ a faire
    n → n+1
fin tant que

Est ce que l'invariant de boucle "après k passages, n vaut k" est un invariant correct ? Il paraît correct selon la définition mais ça me semble trop... simple. De plus, (désolé de poser autant de questions), comment faire dès lors qu'il y a une condition ?

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
t ← 2^n*b
tant que n > 0 faire
    t ← t/2
    n → n−1
    si y < t alors
        z ← 2 ∗ z
    sinon
        z ← 2 ∗ z+1
        y ← y−t
    fin si
fin tant que
afficher (z et y)

J'ai "après k passages, t = 2^n*b*(1/2)^k et n = n-k" mais concernant z et y... difficile de dire quoi que ce soit puisque leur valeur dépend du "tour"...
Merci beaucoup