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?
