Korrektheitsbeweis

1. Was bedeutet Korrektheit?

• Ein Algorithmus heißt korrekt, wenn er für jede zulässige Eingabe in endlicher Zeit (Halteproblem) das gewünschte Ergebnis liefert (partielle bzw. totale Korrektheit).
• Es gibt somit zwei Teilaspekte der Korrektheit:
  1. Terminierung: Der Algorithmus muss für alle Eingaben enden (das Halteproblem).
  2. Partielle Korrektheit: Das ausgegebene Ergebnis muss bei Beendigung korrekt sein.
• WICHTIG: Problembeschreibung muss exakt definiert sein

Unterschied zwischen partielle und totale Korrektheit

• Partielle Korrektheit garantiert, dass das Ergebnis korrekt ist, falls der Algorithmus anhält.
• Totale Korrektheit setzt die partielle Korrektheit voraus, zeigt aber zusätzlich, dass der Algorithmus immer anhält.

2. Das Halteproblem (Terminierung)

• Ein Algorithmus, der nie anhält (z. B. in einer Endlosschleife), kann kein Ergebnis liefern und ist daher nicht korrekt.
• Beispiel: Collatz-Algorithmus – seine Terminierung ist bis heute nicht bewiesen.
• Gegenbeispiel: Algorithmus der ägyptischen Multiplikation hält für alle natürlichen Eingaben n und m, da die Schleifenvariable in jedem Durchlauf strikt sinkt und schließlich die Schleifenbedingung verletzt wird.

Terminierungsbeweis beim Beispiel (ägyptische Multiplikation)

1. Schleifenvariable: x (entspricht n im Input).
2. Eingangsbelegung: x0 = n.
3. Abbruchbedingung: while (x >= 1).
4. Beobachtung:
   • x bleibt eine ganze Zahl.
   • Pro Durchlauf wird x entweder halbiert (wenn gerade) oder (x - 1) halbiert (wenn ungerade). In beiden Fällen verringert sich der Wert garantiert.
   • Nach maximal n Schritten (bzw. einer Funktion, die von n abhängt) wird x so klein, dass die Schleife endet.
5. Ergebnis: Der Algorithmus terminiert bei jeder natürlichen Zahl n.

3. Partielle Korrektheit

Damit der Algorithmus nicht nur anhält, sondern auch das richtige Ergebnis berechnet, muss man zeigen, dass die ausgegebene Variable tatsächlich dem gewünschten Wert entspricht. Beim Beispiel der ägyptischen Multiplikation soll das Produkt n * m berechnet werden.

4. Schleifeninvariante

Definition

• Eine Schleifeninvariante ist eine Eigenschaft (oder ein Wert), die/der vor und nach jedem Schleifendurchlauf gilt.
• Formell heißt das:
  1. Zu Beginn der Schleife (Initialisierung) ist die Invariante erfüllt.
  2. Falls die Invariante vor einem Durchlauf gilt, dann gilt sie auch nach diesem Durchlauf.
  3. Gilt die Invariante noch, wenn die Schleife abbricht, so liefert sie Informationen über den Endzustand.

Beispiel-Invariante bei der ägyptischen Multiplikation

• Man wählt als Schleifeninvariante den Ausdruck

Hier sind x, y und p Variablen, die im Algorithmus in jedem Schleifendurchlauf geändert werden.

• Idee:
  • Durch Halbieren von x und Verdoppeln von y bleibt das Produkt x * y konstant.
  • Falls x ungerade ist, wird ein passender Anteil (y) zu p addiert und gleichzeitig x durch (x - 1) halbiert.
    Dadurch gleicht sich das Produkt wieder aus.
  • Insgesamt bleibt x * y + p vor und nach jedem Schleifendurchlauf gleich.

Beispiel-Invariante bei der Maximumsuche

• Schleifeninvariante
  • Definition: A[max] ist ein größtes Element aus A[1..j-1].
  • Abkürzung: A[1..j-1] bezeichnet das Teilarray von A[1] bis A[j-1].
• Beweis der Schleifeninvariante
  1. Initialisierung (vor der Schleife):
     • Zu Beginn ist j = 2.
     • Das Teilarray A[1..1] enthält nur das erste Element (A[1]).
     • Es gilt: max = 1, also ist A[max] = A[1].
     • Die Invariante gilt, da A[max] das größte Element aus A[1..1] ist.
  2. Erhaltung (während der Schleife):
     • Angenommen, die Invariante gilt zu Beginn eines Schleifendurchlaufs für ein aktuelles j.
     • Es gibt zwei Fälle:
       1. Fall 1: A[j] ≤ A[max]
          • Die Bedingung if A[j] > A[max] wird nicht erfüllt, und max bleibt unverändert.
          • Somit bleibt A[max] das größte Element aus A[1..j].
       2. Fall 2: A[j] > A[max]
          • Die Bedingung wird erfüllt, und max wird auf j gesetzt.
          • Nun ist A[max] = A[j], das größte Element aus A[1..j].
     • In beiden Fällen bleibt die Schleifeninvariante erhalten.
  3. Abbruch (nach der Schleife):
     • Am Ende der Schleife gilt j = length(A) + 1.
     • Die Schleifeninvariante garantiert, dass A[max] das größte Element aus A[1..length(A)] ist.
     • Da max der Index des größten Elements ist, liefert der Algorithmus korrekt max.

5. Induktionsbeweis (Vollständige Induktion)

Um zu zeigen, dass die Schleifeninvariante tatsächlich zu einem korrekten Ergebnis führt, nutzt man meist einen Induktionsbeweis:

1. Induktionsbasis:

   • Man zeigt, dass die Invariante vor dem ersten Schleifendurchlauf gilt (z. B. x0 = n, y0 = m, p0 = 0, sodass x0 * y0 + p0 = n * m + 0).

2. Induktionsschritt:

   • Angenommen, die Invariante hält nach dem i-ten Durchlauf.
   • Dann zeigt man, dass sie auch nach dem (i+1)-ten Durchlauf gilt.
   • Man rechnet also die Änderungen von x, y und p in den zwei Fällen (gerade/ungerade) durch und stellt sicher, dass x * y + p sich nicht ändert.

3. Ergebnis nach Abbruch:

   • Wenn die Schleife beendet ist, gilt x = 0 (bzw. < 1).
   • Die Invariante besagt:$$0\cdot y+p=p.$$
   • Also muss p = n * m sein (da die Invariante mit dem Anfangswert n*m übereinstimmt).