Musterlösung

Schleifeninvariante:
Zu jeder Zeichenkette s, die mindestens i+1 Zeichen umfasst, enthält die Variable back am Ende der i-ten Iteration das kleinste Element der ersten i+1 Zeichen von s.

Beweis durch vollständige Induktion über die Anzahl i der Iterationen:
Induktionsanfang:
Für i=1 wurde back genau dann das Zeichen s[1] zugewiesen, wenn dies kleiner ist als das Zeichen s[0]. Somit ist back das kleinste Element der ersten i+1 Zeichen von s.
Induktionsschritt:
Induktionsvoraussetzung:
Für jeden beliebigen, aber fortan festen Wert von i enthält back nach der i-ten Iteration das kleinste Element der ersten i+1 Zeichen der aus mindestens i+1 Zeichen bestehenden Zeichenkette s.
Induktionsbehauptung:
Dann enthält back nach der (i+1)-ten Iteration für jede Zeichenkette mit mindestens i+2 Zeichen das kleinste Element der ersten i+2 Zeichen von s.
Beweis der Induktionsbehauptung:
Formalisiert bedeutet die Behauptung, dass back(i+1)=min(s[0],...,s[i+1]) zu zeigen ist, wobei mit back(i) der Wert der Variablen back am Ende der i-ten Iteration bezeichnet sei. Allgemein gilt min(s[0],...,s[i+1])=min(min(s[0],...,s[i]),s[i+1]). Aus der Induktionsvoraussetzung wissen wir nun, dass back(i)=min(s[0],...,s[i]) ist, da die Zeichenkette s nach Voraussetzung mindestens i+2, also insbesondere i+1 Zeichen umfasst. Es bleibt also nur noch zu zeigen, dass back(i+1) nach der (i+1)-ten Iteration den kleineren der beiden Werte back(i) bzw. s[i+1] enthält. Aber genau das wird durch die if-Abfrage gewährleistet. Denn dann, und nur dann, wenn s[i+1] echt kleiner ist als der aktuelle Wert von back, wird back durch Zuweisung genau diesen Wertes verändert. Zusammenfassend ist unsere Argumentationskette die folgende:

• min(s[0],...,s[i+1])=min(min(s[0],...,s[i]),s[i+1]) (allgemein gültiger Zusammenhang)
• min(min(s[0],...,s[i]),s[i+1])=min(back(i),s[i+1]) (Induktionsvoraussetzung)
• min(back(i),s[i+1])=back(i+1) (if-Abfrage in der Methode).

Beweis der Korrektheit der Methode:
Gemäß der Abbruchbedingung der for-Schleife wird für jedes der Zeichen s[1],...,s[s.length()-1] der Zeichenkette s eine Iteration der Schleife durchlaufen. Insbesondere steht dann nach der Iteration s.length()-2 gemäß unserer Schleifeninvariante in der Variablen back das kleinste Zeichen der ersten s.length()-1 Zeichen von s. Da die Zeichenkette s nun aber genau s.length()-1 Zeichen besitzt und die Schleife für jedes dieser Zeichen - bis auf das erste - einmal durchlaufen wurde, enthält back am Ende das kleinste Zeichen von s.