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

[Flodelarab]

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.

C'est faux. Prends la fonction "exponentielle de moins x" (=e^-x). Elle est strictement décroissante et toujours positive. Si ta boucle s'arrête lorsque le résultat devient négatif, tu viens de construire une boucle infinie).

[dourouc05]

En gros, si je comprends bien, l'invariant sert à démontrer la correction et le variant la terminaison, c'est ça ?

Un algorithme ne peut pas être correct s'il ne se termine pas (cf. https://fr.wikipedia.org/wiki/Algorithme) ; par contre, un algorithme qui se termine n'est pas forcément correct (par rapport au problème que tu cherches à résoudre, évidemment). Bon, quand tu joues dans la théorie de la complexité avec des machines de Turing, il faut être plus nuancé, mais ça n'est pas du tout du niveau de cet exercice .

Niveau "intuitif", tu peux considérer leur rôle respectif comme ça, mais les deux sont importants pour montrer la correction.

C'est faux. Prends la fonction "exponentielle de moins x" (=e^-x). Elle est strictement décroissante et toujours positive. Si ta boucle s'arrête lorsque le résultat devient négatif, tu viens de construire une boucle infinie).

C'est une question de définition. Une fonction de terminaison ou variant est définie comme une fonction à valeur entière (contrairement à ton exponentielle) positive ou nulle (tant que l'invariant de boucle est vérifié) : grâce à ces deux propriétés, tu peux effectivement prouver que la boucle s'arrête ; si tu n'imposes pas que les valeurs sont entières, tu peux avoir une fonction qui décroît en permanence mais effectue un nombre infini d'itérations (l'ensemble des réels n'étant pas complet). Bien évidemment, ce n'est pas la seule technique de preuve de terminaison, mais ce que tu proposes ne correspond pas au schéma de preuve à l'aide de fonctions de terminaison. (Voir, par exemple, http://www.ulb.ac.be/di/verif/tmassa...hapitre11.html.)

[pseudocode]

C'est faux. Prends la fonction "exponentielle de moins x" (=e^-x). Elle est strictement décroissante et toujours positive. Si ta boucle s'arrête lorsque le résultat devient négatif, tu viens de construire une boucle infinie).

Comme le dit dourouc05, le variant doit être un entier pour éviter le cas que tu cites (=> éviter la "infinite descending chain").

Pour autant, il n'y a pas besoin que ca soit "strictement" décroissant à chaque itération. Il peut y avoir des répétitions de valeur. Il faut juste éviter que ca stagne pour toujours.

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

Un invariant est une propriété de l'état = une propriété des valeurs des variables du programme.

ici "n" n'est pas une variable du programme.
Si tu veux un invariant, tu as par exemple: x=2^((y-1)/10)

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

Le principe c'est que la décroissance du variant prouve qu'on sort de la boucle... et pas l'inverse.

Mais, oui, tu as raison.
Généralement si une condition s'écrit "y>=x", alors on a une valeur V tel que "y=x+V et V>=0".
Reste a construire un variant à partir de V (entier, positif et décroissant).

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.

idem que précédemment: "k" n'est pas une variable du programme.
Là, ca va être dur de trouver un invariant sans connaitre l'état initial (valeurs de n,a,b avant la boucle).

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

L'idée derrière tout ce fatra de variant/invariant c'est de NE PAS chercher le terme général des variables. Donc ne pas chercher que vaut la variable "machin" à la "k-ième itération".

Il faut plutôt chercher "que se passe-t-il a chaque tour de boucle pour mes variables".
Si on reprend ton premier exemple, il faut se dire:
A. au départ, X=Y=1
B. a chaque tour "x est multiplié par 2 et y augmente de 10"

Ce qui est toujours vrai c'est donc "j'ai multiplié 1 par 2 autant de fois que j'ai ajouté 10 à 1"
=> "si X = 1*2*2*2*.... (n fois), alors Y=1+10+10+10+... (n fois aussi)"

=> log2(x/1) = (y-1)/10