Schleifeninvariante bei Sortieralgorithmus

[Mary123]

Hallo,

ich hab schon ein bisschen über Schleifeninvarianten recherchiert und weiß deshalb grob, was damit gemeint ist. Nur "klack" gemacht hat es noch nicht.
Daher wollte ich euch um Hilfe beim Finden der Invariante des folgenden Codes bitten:

public static void Sort (int[]a) {
 
		for (int i = 0; i < a.length; i++) {
			for (int j=0 ; j < a.length; j++) {
				if (a[i] < a[j]) {
					int hilf = a[i];
					a[i] = a[j];
					a[j] = hilf;
				}
			}
		}
 
	}

Es wäre toll, wenn mir jemand einen Denkanstoß geben könnte.
Und dann frage ich mich, ob ich zwei Schleifeninvarianten finden muss, da ich ja eine doppelte Schleife habe.

 

[Firephoenix]

Ich kenne es so, dass man beim Bubblesort eine Invariante für die innere Schleife und eine für die äußere Schleife aufstellt und daraus dann die Korrektheit beweisen kann.

Überleg dir welche Aussagen immer für die Schleifen gelten (ein Anstoß wäre das hier, ich denke da warst du aber schon):
Schleifeninvariante ? Wikipedia

Eine (hier nicht sehr hilfreiche) Invariante die für beide Schleifen gilt wäre z.B.,
dass die Menge der Elemente in dem Array sich nicht ändert (es kommen keine neuen Elemente hinzu und es werden keine Elemente entfernt)

Gruß

 

[Mary123]

Vielen Dank!
Auf Wikipedia war ich natürlich schon

Als Invariante hab ich mir überlegt:
"a[0… i] enthält die kleinsten Werte der Zahlen von 0 bis i sortiert."

Wäre das geeignet bzw realisierbar?

 

[ThreadPool]

Da fehlen IMHO noch ein paar, kurz mal einen Link für Bubblesort ausgegraben

http://www.8bitavenue.com/2012/02/loop-invariant-bubble-sort/