Beweisen Sie mittels einer geeigneten Schleifeninvariante, dass das folgende Programm die Eingabe A sortiert

Question

Aufgabe:

Beweisen Sie mittels einer geeigneten Schleifeninvariante, dass das folgende Programm die Eingabe A sortiert.

1  void up_down ( in t A []){
2        int left = 0 , right = size ( A ) -1;
3        while ( left < right ){
4               for ( int i = left ; i < right ; i ++){
5                       if ( A [ i ] > A [ i +1]){
6                               swap ( A [ i ] , A [ i +1]);
7                       }
8               }
9               for ( int i = right -1; i > left ; i - -){
10                     if ( A [ i ] < A [i -1]){
11                             swap ( A [i -1] , A [ i ]);
12                     }
13               }
14               left ++;
15               right - -;
16       }
17 }

Die Korrektheit der inneren Schleifen muss dabei nicht über Schleifeninvarianten bewiesen werden, es reicht, deren Effekt zu beschreiben und eine korrekte Funktionsweise vorauszusetzen.

Problem:

Mir ist durchaus bewusst, wie das Programm funktioniert und das es die Eingabe A wie behauptet sortiert. Allerdings weiß ich leider nicht wie ich das über Schleifeninvarianten beweise. Könnte mir da bitte jemand helfen?

Answer 1

Antwort mit KI erzeugt

Einführung

Um zu beweisen, dass das Programm die Eingabe \( A \) sortiert, verwenden wir den Ansatz der Schleifeninvarianten. Eine Schleifeninvariante ist eine Bedingung, die zu Beginn und am Ende jeder Iteration einer Schleife wahr ist. Wenn die Schleifeninvariante zu Beginn und am Ende jeder Schleife gültig bleibt und die Schleife schließlich terminiert, können wir zeigen, dass das Programm korrekt ist.

Beschreibung des Programms

Das Programm implementiert eine Art Cocktail Shaker Sort (eine Variante des Bubble Sort), bei der es in zwei Richtungen durch das Array geht.

1. In der ersten inneren Schleife (Zeilen 4 bis 8) wird das größte Element nach rechts „gebubblet“.
2. In der zweiten inneren Schleife (Zeilen 9 bis 13) wird das kleinste Element nach links „gebubblet“.
3. Die \( left \)- und \( right \)-Grenzen werden angepasst (Zeilen 14 und 15), wodurch der Bereich reduziert wird, der in der nächsten Iteration der äußeren Schleife sortiert wird.

Schleifeninvariante für die äußere Schleife

Die äußere Schleife läuft vom Anfang (linke Grenze) bis zum Ende (rechte Grenze) des Arrays, indem die Grenzen \( left \) und \( right \) nach jeder Iteration jeweils um 1 verschoben werden. Unsere Schleifeninvariante für die äußere Schleife lautet:

- Nach jeder Iteration der äußeren Schleife sind die ersten \( left \) Elemente (von \( A[0] \) bis \( A[left-1] \)) und die letzten \( (n - right - 1) \) Elemente (von \( A[right+1] \) bis \( A[n-1] \)) sortiert und an den richtigen Positionen.

Formale Beweisführung

1. Initialisierung:
Zu Beginn der äußeren Schleife sind \( left = 0 \) und \( right = size(A) - 1 \). Das bedeutet, dass der gesamte Bereich des Arrays bearbeitet wird.

2. Erhaltung:
Am Ende jeder Iteration der äußeren Schleife erhöhen wir \( left \) um 1 und verringern \( right \) um 1.
- In der ersten inneren Schleife (Zeilen 4 bis 8) wird sichergestellt, dass nach dem Durchlauf das größte Element im Bereich \( [left, right] \) an der Position \( right \) steht. Damit ist \( A[right] \) korrekt platziert und alle anderen Elemente sind kleiner oder gleich \( A[right] \).
- In der zweiten inneren Schleife (Zeilen 9 bis 13) wird sichergestellt, dass das kleinste Element im Bereich \( [left, right] \) an der Position \( left \) steht. Damit ist \( A[left] \) korrekt platziert und alle anderen Elemente sind größer oder gleich \( A[left] \).

3. Terminierung:
Wenn \( left \geq right \), ist der äußere Bereich vollständig sortiert. Da bei jeder Iteration von \( left \) und \( right \) beide Randbereiche (linke und rechte Grenzen) verkleinert werden, wird die Schleife schließlich stoppen, wenn \( left \) und \( right \) sich treffen oder kreuzen.

Quellcode des Programms:

cpp
void up_down(int A[]) {
    int left = 0, right = size(A) - 1;
    while (left < right) {
        for (int i = left; i < right; i++) {
            if (A[i] > A[i + 1]) {
                swap(A[i], A[i + 1]);
            }
        }
        for (int i = right - 1; i > left; i--) {
            if (A[i] < A[i - 1]) {
                swap(A[i - 1], A[i]);
            }
        }
        left++;
        right--;
    }
}

Zusammenfassung:

- Initialization: Initial \( left = 0 \) und \( right = size(A) - 1 \) bedeutet, dass der gesamte Bereich des Arrays betrachtet wird.
- Maintenance: Jedes Mal, wenn die inneren Schleifen abgeschlossen sind, bewegt sich das größte Element nach rechts und das kleinste nach links, wodurch die Grenzen angepasst werden.
- Termination: Die Schleife stoppt, wenn \( left \geq right \). Zu diesem Zeitpunkt ist das ganze Array sortiert.

Die Schleifeninvariante garantiert, dass unser Algorithmus korrekt arbeitet und das Array \( A \) sortiert.