Je lis « Introduction à l’algorithme » plc. et les auteurs parlent des invariants de boucle, dans le chapitre 2 (tri d’Insertion). Je n’ai aucune idée de ce que cela signifie.
Réponses
Trop de publicités?
En termes simples, une boucle invariante est un prédicat (condition) qui contient pour chaque itération de la boucle. Par exemple, regardons un simple `` boucle qui ressemble à ceci :
Dans cet exemple, il est vrai (pour chaque itération) qui . Un invariant plus faible qui est également vrai, c’est que (parce que c’est la condition de cessation d’emploi !) ou qui `` .
TNi
Points
2766
J'aime cette définition très simple:
Un invariant de boucle est un trouble de la santé [parmi les variables du programme] qui est nécessairement le cas, immédiatement avant et immédiatement après chaque itération d'une boucle. (Notez que cela ne dit rien sur la vérité ou la fausseté de la partie chemin à travers une itération.)
Source: http://www.cs.uofs.edu/~mccloske/courses/cmps144/invariants_lec.html
Par lui-même, un invariant de boucle ne fait pas beaucoup. Toutefois, étant donné approprié invariant, il peut être utilisé pour aider à prouver l'exactitude de l'algorithme. L'exemple simple en CLRS a probablement à voir avec le tri. Par exemple, laissez votre invariant de boucle d'avoir quelque chose comme, au début de la boucle, la première i des entrées 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, la première i des entrées sont triées signifie que le tableau est trié.
Un moyen encore plus simple exemple est illustré à http://academic.evergreen.edu/curricular/dsa01/loops.html.
La façon dont je le comprends un invariant de boucle est systématique, formel outil pour raisonner sur les programmes. Nous faire une seule déclaration que nous nous concentrons sur la preuve de vrai, et nous l'appelons l'invariant de boucle. Ce organise de notre logique. Alors que nous pouvons tout aussi bien argumenter de manière informelle sur l'exactitude de certains algorithme, à l'aide d'un invariant de boucle nous oblige à réfléchir très attentivement et assure notre raisonnement est étanche à l'air.
Robert S. Barnes
Points
17244
Il y a une chose que beaucoup de gens ne réalisent pas tout de suite lorsque vous traitez avec des boucles et des invariants. Ils se confondent entre l'invariant de boucle et la boucle conditionnelle ( l'état qui contrôle la terminaison de la boucle ).
Comme les gens, l'invariant de boucle doit être vrai
- avant la boucle commence
- avant chaque itération de la boucle
- après la boucle s'arrête
( même si elle peut être temporairement faux pendant le corps de la boucle ). D'autre part, la boucle conditionnelle doit être faux après que la boucle se termine, sinon la boucle aurait jamais de fin.
Ainsi, l'invariant de boucle et la boucle conditionnelle doit être de différentes conditions.
Un bon exemple d'un ensemble invariant de boucle est pour les binaires de recherche.
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 - dès le début de la > fin de la boucle termine. Mais pourquoi la boucle correcte? Quel est l'invariant de boucle qui prouve que c'est correct?
L'invariant est la logique de l'énoncé:
if ( A[mid] == a ) then ( start <= mid <= end )
Cette déclaration est une logique de la tautologie - il est toujours vrai dans le contexte de la boucle / algorithme que nous essayons de prouver. Et il fournit des informations utiles sur l'exactitude de la boucle après il se termine.
Si nous revenons parce que nous avons trouvé l'élément dans le tableau l'énoncé est clairement vrai, car si l' A[mid] == a alors a est dans le tableau et en mid doit être entre le début et la fin. Et si la boucle se termine, car start > end puis il y a peut être pas de numéro de tel que start <= mid et mid <= end et, par conséquent, nous savons que l'énoncé A[mid] == a doit être fausse. Toutefois, en raison de la logique globale déclaration est encore vrai dans le null sens. ( Dans la logique de la déclaration, si ( faux), alors ( quelque chose ) est toujours vraie. )
Maintenant, ce sujet ce que j'ai dit à propos de la boucle conditionnelle nécessairement faux 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!? Il est pas vraiment, parce que l'implicite boucle conditionnelle est vraiment while ( A[mid] != a && start <= end ) , mais nous raccourcir le test, puisque la première partie est implicite. Cette condition est clairement faux après la boucle indépendamment de la façon dont la boucle se termine.
Vahid Rafiei
Points
174
À côté de toutes les bonnes réponses, je pense un excellent exemple de la Façon de Penser des Algorithmes, par Jeff Edmonds peut illustrer le concept très bien:
EXEMPLE 1.2.1 "Le Trouvez-Max à Deux Doigts de l'Algorithme"
1) Spécifications: Une entrée de l'instance se compose d'une liste L(1..n) de éléments. La sortie se compose d'un indice i tel que L(i) a maximum de la valeur. S'il existe plusieurs entrées avec cette même valeur, alors tout l'un d'eux est retourné.
2) Étapes de Base: Vous décidez de sur le à deux doigts de la méthode. Votre doigt droit pistes en bas de la liste.
3) Mesure du Progrès: Le progrès est dans quelle mesure le long de la la liste de votre doigt droit.
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 vers le bas un entrée dans la liste. Si votre doigt est maintenant pointer une entrée qui est plus grand que le doigt gauche de l'entrée, puis déplacez votre gauche doigt de votre main droite.
6) Faire des Progrès: Vous faites des progrès, parce que votre doigt 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, la nouvelle gauche doigt élément est Max(vieille gauche doigt élément, un nouvel élément). Par l'invariant de boucle, c'est Max(Max(liste plus courte), un nouvel élément). Mathématiquement, c'est Max(liste plus longue).
8) l'Établissement de l'Invariant de Boucle: Vous d'abord établir l'invariant de boucle par point - ing les deux doigts vers le premier élément.
9) Sortie Condition: Vous avez fait lors de votre doigt droit a fini parcourant la liste.
10) la Fin: À la fin, nous savons que le problème est résolu comme suit. Par la sortie de la condition, votre doigt droit a rencontré tous les les entrées. Par l'invariant de boucle, de votre gauche doigt points au maximum de ces. De retour de cette entrée.
11) la Cessation et durée: Le temps requis est une constante fois la longueur de la liste.
12) Cas particuliers: Vérifier ce qui se passe lorsqu'il y a plusieurs entrées avec la même valeur ou lorsque n = 0 ou n = 1.
13) le Codage et la mise en Œuvre de Détails: ...
14) la Preuve Formelle: l'exactitude de L'algorithme suit à partir de la étapes ci-dessus.
Mark Rushakoff
Points
97350
