Was ist eine Schleifeninvariante?

Ich lese "Einführung in den Algorithmus" von CLRS. In Kapitel 2 erwähnen die Autoren "Schleifeninvarianten". Was ist eine Schleifeninvariante?

Mit einfachen Worten, eine Schleifeninvariante ist ein Prädikat (Bedingung), das für jede Iteration der Schleife gilt. Schauen wir uns zum Beispiel eine einfache forSchleife an, die so aussieht:

int j = 9;
for(int i=0; i<10; i++)  
  j--;

In diesem Beispiel ist es wahr (für jede Iteration), dass i + j == 9. Eine schwächere Invariante, die auch wahr ist, ist das i >= 0 && i <= 10.

Ich mag diese sehr einfache Definition: ( Quelle )

Eine Schleifeninvariante ist eine Bedingung [unter Programmvariablen], die unmittelbar vor und unmittelbar nach jeder Iteration einer Schleife erfüllt sein muss. (Beachten Sie, dass dies während einer Iteration nichts über seine Wahrheit oder Falschheit aussagt.)

Eine Schleifeninvariante allein macht nicht viel. Bei einer geeigneten Invariante kann sie jedoch verwendet werden, um die Richtigkeit eines Algorithmus zu beweisen. Das einfache Beispiel in CLRS hat wahrscheinlich mit Sortieren zu tun. Lassen Sie Ihre Schleifeninvariante beispielsweise so sein, dass zu Beginn der Schleife die ersten iEinträge dieses Arrays sortiert werden. Wenn Sie beweisen können, dass dies tatsächlich eine Schleifeninvariante ist (dh dass sie vor und nach jeder Schleifeniteration gilt), können Sie damit die Richtigkeit eines Sortieralgorithmus beweisen: Am Ende der Schleife ist die Schleifeninvariante immer noch erfüllt und der Zähler iist die Länge des Arrays. Daher werden die ersten iEinträge sortiert, dh das gesamte Array wird sortiert.

Ein noch einfacheres Beispiel: Schleifeninvarianten, Korrektheit und Programmableitung .

Die Art und Weise, wie ich eine Schleifeninvariante verstehe, ist ein systematisches, formales Werkzeug, um über Programme nachzudenken. Wir machen eine einzige Aussage, die wir darauf konzentrieren, die Wahrheit zu beweisen, und nennen sie die Schleifeninvariante. Dies organisiert unsere Logik. Während wir genauso gut informell über die Richtigkeit eines Algorithmus streiten können, zwingt uns die Verwendung einer Schleifeninvariante, sehr sorgfältig zu überlegen, und stellt sicher, dass unsere Argumentation luftdicht ist.

Es gibt eine Sache, die viele Menschen beim Umgang mit Schleifen und Invarianten nicht sofort erkennen. Sie werden zwischen der Schleifeninvariante und der Schleifenbedingung (der Bedingung, die die Beendigung der Schleife steuert) verwechselt.

Wie die Leute betonen, muss die Schleifeninvariante wahr sein

1. bevor die Schleife beginnt
2. vor jeder Iteration der Schleife
3. nachdem die Schleife beendet ist

(obwohl es während des Körpers der Schleife vorübergehend falsch sein kann). Auf der anderen Seite der Schleife bedingte müssen , nachdem die Schleife beendet falsch sein, sonst wäre die Schleife nie enden.

So ist die Schleifeninvariante und die Schleife bedingte müssen verschiedene Bedingungen geknüpft werden.

Ein gutes Beispiel für eine komplexe Schleifeninvariante ist die binäre Suche.

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

}

Die Schleifenbedingung scheint also ziemlich einfach zu sein - wenn Start> Ende, endet die Schleife. Aber warum ist die Schleife richtig? Was ist die Schleifeninvariante, die ihre Richtigkeit beweist?

Die Invariante ist die logische Aussage:

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

Diese Aussage ist eine logische Tautologie - sie gilt immer im Kontext der spezifischen Schleife / des Algorithmus, die wir zu beweisen versuchen . Außerdem werden nützliche Informationen zur Richtigkeit der Schleife nach deren Beendigung bereitgestellt.

Wenn wir zurückkehren, weil wir das Element im Array gefunden haben, ist die Aussage eindeutig wahr, da if A[mid] == adann aim Array ist und midzwischen Anfang und Ende liegen muss. Und wenn die Schleife beendet , weil start > enddann kann es keine Zahl , so dass start <= mid und mid <= end und deshalb wissen wir , dass die Aussage A[mid] == afalsch sein muss. Infolgedessen ist die logische Gesamtaussage jedoch immer noch im Null-Sinne wahr. (In der Logik ist die Aussage wenn (falsch) dann (etwas) immer wahr.)

Was ist nun mit dem, was ich über die Schleifenbedingung gesagt habe, die notwendigerweise falsch ist, wenn die Schleife endet? Es sieht so aus, als ob, wenn das Element im Array gefunden wird, die Schleifenbedingung wahr ist, wenn die Schleife endet!? Es ist eigentlich nicht so, weil die implizite Schleifenbedingung wirklich ist, while ( A[mid] != a && start <= end )aber wir verkürzen den tatsächlichen Test, da der erste Teil impliziert ist. Diese Bedingung ist nach der Schleife eindeutig falsch, unabhängig davon, wie die Schleife endet.

Frühere Antworten haben eine Schleifeninvariante auf sehr gute Weise definiert.

Im Folgenden wird beschrieben, wie Autoren von CLRS Schleifeninvarianten verwendeten, um die Richtigkeit zu beweisen der Einfügungssortierung .

Einfügungssortierungsalgorithmus (wie im Buch angegeben):

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

Schleifeninvariante in diesem Fall: Unterarray [1 bis j-1] wird immer sortiert.

Lassen Sie uns dies nun überprüfen und beweisen, dass der Algorithmus korrekt ist.

Initialisierung : Vor der ersten Iteration ist j = 2. Subarray [1: 1] ist also das zu testende Array. Da es nur ein Element hat, ist es sortiert. Somit ist die Invariante erfüllt.

Wartung : Dies kann leicht überprüft werden, indem die Invariante nach jeder Iteration überprüft wird. In diesem Fall ist es zufrieden.

Beendigung : Dies ist der Schritt, in dem wir die Richtigkeit des Algorithmus beweisen.

Wenn die Schleife endet, ist der Wert von j = n + 1. Wieder ist die Schleifeninvariante erfüllt. Dies bedeutet, dass das Subarray [1 bis n] sortiert werden sollte.

Das wollen wir mit unserem Algorithmus machen. Somit ist unser Algorithmus korrekt.

Neben all den guten Antworten kann Jeff Edmonds ein großartiges Beispiel aus How to Think About Algorithms von Jeff Edmonds sehr gut veranschaulichen:

BEISPIEL 1.2.1 "Der Find-Max-Zwei-Finger-Algorithmus"

1) Spezifikationen: Eine Eingabeinstanz besteht aus einer Liste L (1..n) von Elementen. Die Ausgabe besteht aus einem Index i, so dass L (i) den Maximalwert hat. Wenn es mehrere Einträge mit demselben Wert gibt, wird einer von ihnen zurückgegeben.

2) Grundlegende Schritte: Sie entscheiden sich für die Zwei-Finger-Methode. Ihr rechter Finger läuft die Liste hinunter.

3) Maß für den Fortschritt: Das Maß für den Fortschritt ist, wie weit Ihr rechter Finger entlang der Liste ist.

4) Die Schleifeninvariante: Die Schleifeninvariante gibt an, dass Ihr linker Finger auf einen der größten Einträge zeigt, auf die Ihr rechter Finger bisher gestoßen ist.

5) Hauptschritte: Bei jeder Iteration bewegen Sie Ihren rechten Finger um einen Eintrag in der Liste. Wenn Ihr rechter Finger jetzt auf einen Eintrag zeigt, der größer als der Eintrag des linken Fingers ist, bewegen Sie Ihren linken Finger so, dass er mit Ihrem rechten Finger übereinstimmt.

6) Fortschritte machen: Sie machen Fortschritte, weil Ihr rechter Finger einen Eintrag bewegt.

7) Schleifeninvariante beibehalten: beibehalten Sie wissen, dass die Schleifeninvariante wie folgt beibehalten wurde. Für jeden Schritt ist das neue linke Fingerelement Max (altes linkes Fingerelement, neues Element). Bei der Schleifeninvariante ist dies Max (Max (kürzere Liste), neues Element). Mathematisch gesehen ist dies Max (längere Liste).

8) Festlegen der Schleifeninvariante: Sie legen die Schleifeninvariante zunächst fest, indem Sie mit beiden Fingern auf das erste Element zeigen.

9) Ausgangsbedingung: Sie sind fertig, wenn Ihr rechter Finger die Liste durchlaufen hat.

10) Ende: Am Ende wissen wir, dass das Problem wie folgt gelöst ist. Bei der Ausgangsbedingung hat Ihr rechter Finger alle Einträge gefunden. Durch die Schleifeninvariante zeigt Ihr linker Finger auf das Maximum davon. Geben Sie diesen Eintrag zurück.

11) Beendigung und Laufzeit: Die erforderliche Zeit beträgt einige konstante Zeiten der Länge der Liste.

12) Sonderfälle: Überprüfen Sie, was passiert, wenn mehrere Einträge mit demselben Wert vorhanden sind oder wenn n = 0 oder n = 1 ist.

13) Codierungs- und Implementierungsdetails: ...

14) Formaler Beweis: Die Richtigkeit des Algorithmus ergibt sich aus den obigen Schritten.

Es ist zu beachten, dass eine Schleifeninvariante beim Entwurf iterativer Algorithmen hilfreich sein kann, wenn sie als Behauptung betrachtet wird, die wichtige Beziehungen zwischen den Variablen ausdrückt, die zu Beginn jeder Iteration wahr sein müssen und wenn die Schleife endet. Wenn dies zutrifft, ist die Berechnung auf dem Weg zur Effektivität. Wenn false, ist der Algorithmus fehlgeschlagen.

Invariant bedeutet in diesem Fall eine Bedingung, die an einem bestimmten Punkt in jeder Schleifeniteration erfüllt sein muss.

Bei der Vertragsprogrammierung ist eine Invariante eine Bedingung, die (vertraglich) vor und nach dem Aufruf einer öffentlichen Methode erfüllt sein muss.

Die Bedeutung der Invariante ändert sich nie

Hier bedeutet die Schleifeninvariante "Die Änderung, die mit der Variablen in der Schleife geschieht (Inkrementieren oder Dekrementieren), ändert nicht die Schleifenbedingung, dh die Bedingung ist erfüllt", so dass das Konzept der Schleifeninvariante gekommen ist

Die Eigenschaft "Schleifeninvariante" ist eine Bedingung, die für jeden Schritt einer Schleifenausführung gilt (dh für Schleifen, while-Schleifen usw.).

Dies ist wichtig für einen schleifeninvarianten Beweis, bei dem gezeigt werden kann, dass ein Algorithmus korrekt ausgeführt wird, wenn diese schleifeninvariante Eigenschaft bei jedem Schritt seiner Ausführung gilt.

Damit ein Algorithmus korrekt ist, muss die Schleifeninvariante wie folgt lauten:

Initialisierung (der Anfang)

Wartung (jeder Schritt danach)

Kündigung (wenn es fertig ist)

Dies wird verwendet, um eine Reihe von Dingen zu bewerten, aber das beste Beispiel sind gierige Algorithmen für das Durchlaufen gewichteter Graphen. Damit ein gieriger Algorithmus eine optimale Lösung liefert (ein Pfad über das Diagramm), muss er alle Knoten auf dem Pfad mit der geringstmöglichen Gewichtung verbinden.

Somit ist die schleifeninvariante Eigenschaft, dass der eingeschlagene Pfad das geringste Gewicht hat. Zu Beginn haben wir keine Kanten hinzugefügt, daher ist diese Eigenschaft wahr (in diesem Fall nicht falsch). Bei jedem Schritt folgen wir der Kante mit dem niedrigsten Gewicht (dem gierigen Schritt), also nehmen wir wieder den Pfad mit dem niedrigsten Gewicht. Am Ende haben wir den Pfad mit der niedrigsten Gewichtung gefunden, sodass unser Eigentum auch wahr ist.

Wenn ein Algorithmus dies nicht tut, können wir beweisen, dass er nicht optimal ist.

Es ist schwierig zu verfolgen, was mit Schleifen passiert. Schleifen, die nicht oder ohne Erreichen ihres Zielverhaltens beendet werden, sind ein häufiges Problem bei der Computerprogrammierung. Schleifeninvarianten helfen. Eine Schleifeninvariante ist eine formale Aussage über die Beziehung zwischen Variablen in Ihrem Programm, die unmittelbar vor dem Ausführen der Schleife (Festlegen der Invariante) und jedes Mal durch die Schleife (Beibehalten der Invariante) am Ende der Schleife erneut gilt ). Hier ist das allgemeine Muster der Verwendung von Schleifeninvarianten in Ihrem Code:

... // die Schleifeninvariante muss hier wahr sein,
während (TESTBEDINGUNG) {
// oben in der Schleife
...
// unten in der Schleife
// die Schleifeninvariante muss hier wahr sein
}
// Termination + Schleifeninvariante = Ziel
...
Zwischen dem oberen und unteren Ende der Schleife werden vermutlich Fortschritte beim Erreichen des Ziels der Schleife erzielt. Dies könnte die Invariante stören (falsch machen). Der Punkt der Schleifeninvarianten ist das Versprechen, dass die Invariante wiederhergestellt wird, bevor der Schleifenkörper jedes Mal wiederholt wird. Dies hat zwei Vorteile:

Die Arbeit wird nicht auf komplizierte, datenabhängige Weise auf den nächsten Durchgang übertragen. Jeder Durchgang durch die Schleife ist unabhängig von allen anderen, wobei die Invariante dazu dient, die Durchgänge zu einem funktionierenden Ganzen zusammenzufügen. Die Begründung, dass Ihre Schleife funktioniert, reduziert sich auf die Begründung, dass die Schleifeninvariante bei jedem Durchlauf durch die Schleife wiederhergestellt wird. Dies unterteilt das komplizierte Gesamtverhalten der Schleife in kleine einfache Schritte, die jeweils separat betrachtet werden können. Die Testbedingung der Schleife ist nicht Teil der Invariante. Es ist das, was die Schleife beendet. Sie betrachten zwei Dinge getrennt: warum die Schleife jemals enden sollte und warum die Schleife ihr Ziel erreicht, wenn sie endet. Die Schleife wird beendet, wenn Sie sich jedes Mal durch die Schleife der Erfüllung der Beendigungsbedingung nähern. Es ist oft leicht, dies sicherzustellen: z Verschieben einer Zählervariablen um eins, bis sie eine feste Obergrenze erreicht. Manchmal ist die Begründung für die Kündigung schwieriger.

Die Schleifeninvariante sollte so erstellt werden, dass das Ziel erreicht wird, wenn die Beendigungsbedingung erreicht ist und die Invariante wahr ist:

Invariante + Beendigung => Ziel
Es erfordert Übung, einfache und verwandte Invarianten zu erstellen, die die gesamte Zielerreichung mit Ausnahme der Beendigung erfassen. Es ist am besten, mathematische Symbole zu verwenden, um Schleifeninvarianten auszudrücken. Wenn dies jedoch zu überkomplizierten Situationen führt, verlassen wir uns auf klare Prosa und gesunden Menschenverstand.

Entschuldigung, ich habe keine Kommentarberechtigung.

@ Thomas Petricek wie du erwähnt hast

Eine schwächere Invariante, die auch wahr ist, ist, dass i> = 0 && i <10 (weil dies die Fortsetzung ist!) "

Wie ist es eine Schleifeninvariante?

Ich hoffe, ich liege nicht falsch, soweit ich verstehe ^[1] , wird die Schleifeninvariante am Anfang der Schleife (Initialisierung) wahr sein, sie wird vor und nach jeder Iteration (Wartung) wahr sein und sie wird auch danach wahr sein die Beendigung der Schleife (Beendigung) . Aber nach der letzten Iteration wird i 10. Also wird die Bedingung i> = 0 && i <10 falsch und beendet die Schleife. Es verletzt die dritte Eigenschaft (Termination) der Schleifeninvariante.

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

Schleifeninvariante ist eine mathematische Formel wie (x=y+1). In diesem Beispiel xund yrepräsentieren zwei Variablen in einer Schleife. In Anbetracht der sich ändernden Verhalten dieser Variablen während der Ausführung des Codes, ist es fast unmöglich , alle möglich zu testen xund yWerte und sehen , ob sie irgendwelche Fehler produzieren. Nehmen wir an, es xist eine ganze Zahl. Ganzzahl kann 32-Bit-Speicherplatz im Speicher enthalten. Wenn diese Anzahl überschritten wird, tritt ein Pufferüberlauf auf. Wir müssen also sicher sein, dass der Code während der Ausführung dieses Codes niemals überschritten wird. Dazu müssen wir eine allgemeine Formel verstehen, die die Beziehung zwischen Variablen zeigt. Schließlich versuchen wir nur, das Verhalten des Programms zu verstehen.

Mit einfachen Worten, es ist eine LOOP-Bedingung, die in jeder Schleifeniteration wahr ist:

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

Darin können wir sagen, Zustand von i ist i<10 and i>=0

Eine Schleifeninvariante ist eine Behauptung, die vor und nach der Ausführung der Schleife wahr ist.

Bei der linearen Suche (gemäß der im Buch angegebenen Übung) müssen wir den Wert V in einem bestimmten Array finden.

Es ist einfach, das Array von 0 <= k <Länge abzutasten und jedes Element zu vergleichen. Wenn V gefunden wurde oder wenn das Scannen die Länge des Arrays erreicht, beenden Sie einfach die Schleife.

Nach meinem Verständnis im obigen Problem-

Schleifeninvarianten (Initialisierung): V wird in der k - 1 - Iteration nicht gefunden. Bei der ersten Iteration wäre dies -1, daher können wir sagen, dass V an Position -1 nicht gefunden wurde

Wartung: In der nächsten Iteration gilt V, das in k-1 nicht gefunden wurde

Terminierung: Wenn V in k-Position gefunden wird oder k die Länge des Arrays erreicht, beenden Sie die Schleife.