Ce qui est un invariant de boucle?

J'aime cette définition très simple: (source)

Un invariant de boucle est une condition [parmi les variables de programme] qui est nécessairement vraie immédiatement avant et immédiatement après chaque itération d'une boucle. (Notez que cela ne dit rien de sa vérité ou de sa fausseté à travers une itération.)

En soi, un invariant de boucle ne fait pas grand-chose. Cependant, étant donné un invariant approprié, il peut être utilisé pour aider à prouver l'exactitude d'un algorithme. Simple exemple dans CLRS a probablement à voir avec le tri. Par exemple, laissez votre invariant de boucle être quelque chose comme, au début de la boucle, les premières entrées i de ce tableau sont triées. Si vous pouvez prouver que c'est bien un invariant de boucle (c'est à dire qu'il détient avant et après chaque itération de boucle), vous pouvez l'utiliser pour prouver la justesse d'un algorithme de tri: à la fin de la boucle, l'invariant de boucle est toujours satisfait, et le compteur i est la longueur du tableau. Par conséquent, l' les premières entrées i sont triées signifie que le tableau entier est trié.

Un exemple encore plus simple: Boucle les Invariants, L'exactitude et la dérivation de programme .

La façon dont je comprends un invariant de boucle est comme un outil systématique et formel pour raisonner sur les programmes. Nous faisons une seule déclaration que nous nous concentrons sur la preuve de la vérité, et nous l'appelons la boucle invariante. Cela organise notre logique. Alors que nous pouvons tout aussi bien discuter de manière informelle sur l'exactitude de certains algorithmes, en utilisant une boucle invariant nous oblige à réfléchir très attentivement et assure que notre raisonnement est hermétique.

Il y a une chose que beaucoup de gens ne réalisent pas tout de suite lorsqu'ils traitent des boucles et des invariants. Ils sont confus entre l'invariant de boucle, et la boucle conditionnelle (la condition qui contrôle la fin de la boucle ).

Comme les gens le soulignent, l'invariant de boucle doit être vrai

1. avant le début de la boucle
2. avant chaque itération de la boucle
3. après la fin de la boucle

(bien qu'il puisse Temporairement être faux pendant le corps de la boucle ). D'autre part, la boucle conditionnelle doit être false après la fin de la boucle, sinon la boucle ne se terminerait jamais.

Ainsi, l'invariant de boucle et la boucle conditionnelle doit être différentes conditions.

Un bon exemple d'invariant de boucle complexe est pour la recherche binaire.

bsearch(type A[], type a) {
start = 1, end = length(A)

    while ( start <= end ) {
        mid = floor(start + end / 2)

        if ( A[mid] == a ) return mid
        if ( A[mid] > a ) end = mid - 1
        if ( A[mid] < a ) start = mid + 1

    }
    return -1

}

Donc la boucle conditionnelle semble assez simple - quand start > end la boucle se termine. Mais pourquoi est la boucle correcte? Quel est l'invariant de boucle qui prouve son exactitude?

L'invariant est l'énoncé logique:

if ( A[mid] == a ) then ( start <= mid <= end )

Cette déclaration est une tautologie logique - elle est toujours vraie dans le contexte de la boucle / algorithme spécifique que nous essayons de prouver . Et il fournit des informations utiles sur l'exactitude de la boucle après sa fin.

Si nous retournons parce que nous avons trouvé l'élément dans le tableau alors l'instruction est clairement vraie, puisque si A[mid] == a, puis a est dans le tableau et mid doit être entre le début et la fin. Et si la boucle se termine parce que start > end alors il ne peut y avoir aucun nombre tel que start <= mid et mid <= end et donc nous savons que la déclaration A[mid] == a doit être fausse. Cependant, par conséquent, l'instruction logique globale est toujours vraie dans le sens nul. (En logique, l'instruction if (false) then (something) est toujours vraie. )

Maintenant, qu'en est-il de ce que j'ai dit à propos de la boucle conditionnelle nécessairement fausse lorsque la boucle se termine? Ça ressemble quand l'élément est trouvé, dans le tableau, puis la boucle conditionnelle est vraie lorsque la boucle se termine!? Ce n'est pas le cas, car la boucle implicite conditionnelle est vraiment while ( A[mid] != a && start <= end ) mais nous raccourcions le test réel puisque la première partie est implicite. Ce conditionnel est clairement faux après la boucle, quelle que soit la façon dont la boucle se termine.

Les réponses précédentes ont défini un Invariant de boucle d'une très bonne manière.

Maintenant, laissez-moi essayer d'expliquer comment les auteurs de CLRS ont utilisé des Invariants de boucle pour prouver l'exactitude du tri D'Insertion.

Algorithme de tri D'Insertion (comme indiqué dans le livre):

INSERTION-SORT(A)
    for j ← 2 to length[A]
        do key ← A[j]
        // Insert A[j] into the sorted sequence A[1..j-1].
        i ← j - 1
        while i > 0 and A[i] > key
            do A[i + 1] ← A[i]
            i ← i - 1
        A[i + 1] ← key

Invariant de boucle dans ce cas (Source: clrs book): le sous-tableau[1 à j-1] est toujours trié.

Maintenant, vérifions ceci et prouvons que l'algorithme est correct.

Initialisation: Avant le première itération j=2. Donc Subarray [1: 1] est le tableau à être tested.As il n'a qu'un seul élément donc il est trié.Ainsi Invariant est satisfait.

Maintanence : ceci peut être facilement vérifié en vérifiant l'invariant après chaque iteration.In ce cas, il est satisfait.

La Résiliation: C'est l'étape où nous allons prouver l'exactitude de l'algorithme.

Lorsque la boucle se termine alors la valeur de j=n+1. Encore une fois, l'invariant de boucle est satisfait.Cela signifie que Le sous-tableau[1 À n] doit être trié.

C'est Ce que nous voulons faire avec notre Algorithme.Ainsi notre algorithme est correct.

À côté de toutes les bonnes réponses, je suppose un excellent exemple de Comment penser aux algorithmes, par Jeff Edmonds peut très bien illustrer le concept:

Exemple 1.2.1 "L'algorithme Find-Max à deux doigts"

1) Spécifications: une instance d'entrée se compose D'une liste L (1..n) des élément. La sortie se compose d'un index i tel que L (i) a un maximum valeur. S'il y a plusieurs entrées avec cette même valeur, alors tout l'un d'eux est retourner.

2) étapes de base: vous décidez de la méthode à deux doigts. Ton doigt droit pistes en bas de la liste.

3) Mesure des progrès: la mesure des progrès est de savoir jusqu'à quel point le la liste de votre doigt est.

4) L'Invariant de Boucle: L'invariant de boucle indique que votre doigt gauche points à l'une des plus grandes entrées rencontré jusqu'à présent par votre doigt droit.

5) principales étapes: chaque itération, vous déplacez votre doigt droit vers le bas un entrée dans la liste. Si votre doigt droit pointe maintenant vers une entrée c'est plus grand que l'entrée du doigt gauche, puis déplacez votre gauche doigt de votre main droite.

6) Faire des progrès: vous faites des progrès parce que votre doigt droit se déplace une entrée.

7) Maintenir l'Invariant de Boucle:, Vous savez que l'invariant de boucle a été maintenu comme suit. Pour chaque étape, le nouvel élément de doigt gauche est Max(ancien élément de doigt gauche, nouvel élément). Par l'invariant de boucle, C'est Max(Max(liste plus courte), nouvel élément). Mathématiquement, c'est Max(liste plus longue).

8) Etablissement de L'Invariant de boucle: vous établissez initialement l'invariant de boucle en pointant les deux doigts vers le premier élément.

9) condition de sortie: vous avez terminé lorsque votre doigt droit a terminé parcourant la liste.

10) Fin: en fin de compte, nous savons que le problème est résolu comme suit. Par la condition de sortie, votre doigt droit a rencontré tous les le entrée. Par l'invariant de boucle, votre doigt gauche pointe au maximum de ces. Retournez cette entrée.

11) Temps de terminaison et de fonctionnement: le temps requis est une constante fois la longueur de la liste.

12) cas particuliers: vérifiez ce qui se passe lorsqu'il y a plusieurs entrées avec la même valeur ou lorsque n = 0 ou n = 1.

13) Détails de codage et de mise en œuvre: ...

14) preuve formelle: l'exactitude de l'algorithme découle de la étapes ci-dessus.

Il convient de noter qu'un Invariant de boucle peut aider à la conception d'algorithmes itératifs lorsqu'il est considéré comme une assertion qui exprime des relations importantes entre les variables qui doivent être vraies au début de chaque itération et lorsque la boucle se termine. Si cela est valable, le calcul est sur la voie de l'efficacité. Si la valeur est false, alors l'algorithme a échoué.

Invariant dans ce cas signifie une condition qui doit être vraie à un certain point dans chaque itération de boucle.

En programmation contractuelle, un invariant est une condition qui doit être vraie (par contrat) avant et après l'appel d'une méthode publique.

La signification de invariant n'est jamais changer

Ici, l'invariant de boucle signifie "le changement qui arrive à la variable dans la boucle (incrément ou décrément) ne change pas la condition de boucle, c'est-à-dire que la condition est satisfaisante" de sorte que le concept invariant de boucle est venu

Il est difficile de garder une trace de ce qui se passe avec les boucles. Boucles qui ne se terminent pas ou se terminent sans atteindre leur comportement objectif est un problème commun dans la programmation informatique. Les invariants de boucle aident. Un invariant de boucle est une déclaration formelle sur la relation entre les variables de votre programme qui est vraie juste avant que la boucle ne soit exécutée (établissant l'invariant) et est vraie à nouveau au bas de la boucle, à chaque fois dans la boucle (maintenant l'invariant). Ici, c'est le modèle général de L'utilisation des Invariants de boucle dans votre code:

... // L'Invariant de boucle doit être vrai ici
while (condition D'essai ) {
// haut de la boucle
...
// bas de la boucle
// L'Invariant de boucle doit être vrai ici
}
// Terminaison + Invariant De Boucle = Objectif
...
Entre le haut et le bas de la boucle, des progrès sont probablement faits vers l'atteinte de l'objectif de la boucle. Cela pourrait déranger (faire false) l'invariant. Le point des Invariants de boucle est la promesse que l'invariant sera restauré avant de répéter le corps de la boucle à chaque fois. Il y a deux avantages à cela:

Le travail n'est pas reporté au passage suivant de manière compliquée et dépendante des données. Chaque passage à travers la boucle en indépendant de tous les autres, avec l'invariant servant à lier les passes ensemble dans un ensemble de travail. Le raisonnement selon lequel votre boucle fonctionne est réduit au raisonnement selon lequel l'invariant de boucle est restauré avec chaque passage à travers la boucle. Cela brise le comportement global compliqué de la boucle en petites étapes simples, chacune pouvant être considérée séparément. La condition de test de la boucle ne fait pas partie de l'invariant. C'est ce qui fait la boucle à la fin. Vous considérez séparément deux choses: pourquoi la boucle devrait jamais se terminer, et pourquoi la boucle atteint son objectif quand elle se termine. La boucle se terminera si chaque fois que vous traversez la boucle, vous vous rapprochez de la condition de terminaison. Il est souvent facile à assurer: par exemple, stepping une variable de compteur par un jusqu'à ce qu'il atteigne une limite supérieure fixe. Parfois, le raisonnement derrière la résiliation est plus difficile.

L'invariant de boucle doit être créé de telle sorte que lorsque la condition de terminaison est atteinte, et que l'invariant est vrai, alors le but est atteint:

Invariant + terminaison = > objectif
Il faut de la pratique pour créer des invariants qui sont simples et se rapportent qui capturent toute la réalisation du but, sauf pour la fin. Il est préférable d'utiliser des symboles mathématiques pour exprimer des invariants de boucle, mais lorsque cela conduit à des situations trop compliquées, nous nous appuyons sur la prose claire et le bon sens.

Désolé je n'ai pas de commentaire autorisation.

@ Tomas Petricek comme vous l'avez mentionné

Un invariant plus faible qui est également vrai est que i > = 0 & & i

Comment c'est un invariant de boucle?

J'espère que je ne me trompe pas, comme je le comprends^[1], invariant de Boucle sera le cas au début de la boucle (Initialisation), il sera vrai avant et après chaque itération (Maintenance) , il sera également vrai après la fin de la boucle (terminaison) . Mais après la dernière itération, Je devient 10. Ainsi, la condition i > = 0 & & i

[1] http://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html

La propriété invariante de boucle est une condition qui tient pour chaque étape d'une exécution de boucles (ie. pour les boucles, tandis que les boucles, etc.)

Ceci est essentiel à une preuve invariante de boucle, où l'on est capable de montrer qu'un algorithme s'exécute correctement si, à chaque étape de son exécution, cette propriété invariante de boucle est conservée.

Pour qu'un algorithme soit correct, L'Invariant de boucle doit tenir à:

Initialisation (le début)

Maintenance (chaque étape après)

Terminaison (quand elle est terminée)

Ceci est utilisé pour évaluer un tas de choses, mais le meilleur exemple est les algorithmes gourmands pour la traversée de graphe pondérée. Pour qu'un algorithme gourmand produise une solution optimale (un chemin à travers le graphique), il doit atteindre connecter tous les nœuds dans le chemin de poids le plus bas possible.

Ainsi, la propriété invariante de boucle est que le chemin pris a le moins de poids. Au début de , nous n'avons ajouté aucun bord, donc cette propriété est vrai (il n'est pas faux, dans ce cas). À chaque étape , nous suivons le bord de poids le plus bas (l'étape gourmande), donc encore une fois nous prenons le chemin de poids le plus bas. À la fin , nous avons trouvé le chemin pondéré le plus bas, donc notre propriété est également vraie.

Si un algorithme ne le fait pas, nous pouvons prouver qu'il n'est pas optimal.

L'invariant de boucle est une formule mathématique telle que (x=y+1). Dans cet exemple, x et y représentent deux variables dans une boucle. Compte tenu du comportement changeant de ces variables tout au long de l'exécution du code, il est presque impossible de tester toutes les valeurs possibles de x et y et de voir si elles produisent un bug. Disons que x est un entier. Integer peut contenir 32 bits d'espace dans la mémoire. Si ce nombre dépasse, un débordement de tampon se produit. Nous devons donc nous assurer que tout au long de la exécution du code, il ne dépasse jamais cet espace. pour cela, nous devons comprendre une formule générale qui montre la relation entre les variables. Après tout, nous essayons juste de comprendre le comportement du programme.

En termes simples, c'est une condition de boucle qui est vraie dans chaque itération de boucle:

for(int i=0; i<10; i++)
{ }

En cela, nous pouvons dire que l'état de i est i<10 and i>=0

Un invariant de boucle est une assertion qui est vraie avant et après l'exécution de la boucle.

En recherche linéaire (selon l'exercice donné dans le livre), nous devons trouver la valeur V dans un tableau donné.

C'est simple comme balayer le tableau à partir de 0

Selon ma compréhension dans le problème ci-dessus-

Invariants De Boucle (Initialisation): V n'est pas trouvé dans l'itération k-1. Toute première itération, ce serait -1 donc nous pouvons dire V pas trouvé à la position -1

Maintenance: Dans l'itération suivante, V introuvable dans k-1 est vrai

Terminatation: Si V trouvé en position k ou k atteint la longueur du tableau, terminez la boucle.