Korrektheitsbeweis Algorithmus?
Hallo liebe Community,
ich habe eine Aufgabe bekommen in welcher ich Pseudocode entwickeln soll. Meinem Algorithmus wird ein Array an Zahlen gegeben A[1, n] mit n Einträgen. Ich soll in diesem Array die Senken zählen. Eine Senke ist dabei eine Position i [2, n - 1] für die folgendes gilt: A[i - 1] > A[i] < A[i + 1].
Meiner Auffasung nach bedeutet das nun, dass z.B. das Array [1, 3, 2, 4, 3, 5] zwei Senken hat. Nämlich einmal der dritte Eintrag und der fünfte Eintrag.
Mein Pseudocode sieht folgendermaßen aus:
Input: A[1, n] mit n Einträgen
Output: Anzahl der Senken
counter := 0
for j := 2 to n - 1 do
val := A[j]
if val < A[j - 1] and val > A[j + 1] do
counter := counter + 1
Mein Java Code dazu sieht folgendermaßen aus:
public static int countSenken(int[] arr) {
int counter = 0;
for (int i = 1; i < arr.length - 1; i++) {
int val = arr[i];
if (val < arr[i - 1] && val < arr[i + 1]) {
counter++;
}
}
}
Nun soll ich die Korrektheit meines Algorithmus' beweisen. Wir haben das schonmal an dem Beispiel des Insertionsort Algorithmus' gemacht. Die herangehensweise ist ja eigentlich, dass man eine Schleifeninvariante aufstellt und diese dann mittels Induktion beweist. Mein Problem ist jetzt aber, dass ich diese Schleifeninvariante nicht aufstellen kann. Beim Insertionsort, da beweist man ja die Sortiertheit und da verändert sich ja das Array. Aber bei diesem Algorithmus jetzt da verändert sich das Array ja gar nicht.
Ich weiß halt, dass n >= 3 sein muss damit der Algorithmus überhaupt funktioniert. Kann mir vielleicht jemand einen Ansatz geben wie ich die Korrektheit beweise?
Ich wäre euch allen sehr dankbar :)
1 Antwort
if val < A[j - 1] and val > A[j + 1] do
Das '>' müsste ein '<' sein.
Kann mir vielleicht jemand einen Ansatz geben wie ich die Korrektheit beweise?
Es verändert sich die Schleifenvariable und der Counter.
Es wird immer ein Fenster aus drei Array-Werten betrachtet, welches sich mit jedem Schleifendurchlauf um eine Stelle weiterschiebt.
Als Invariante könnte ich mir folgendes vorstellen:
Wenn in dem Fenster eine Senke ist, dann wird diese gefunden.
Wenn eine Senke gefunden wurde, dann erhöht sich der Counter.
Zudem noch Invarianten, um zu zeigen, dass die Schleife terminiert und keine Senke doppelt zählt, das sollte allerdings trivial sein.