Schleifeninvariante - Beweis auf Korrektheit

Suchproblem:

Eingabe: Eine Sequenz von n Zahlen A = <a1,a2,...,an> und Wert v.

Ausgabe: Ein Index i mit v = A[i], falls v in A vorkommt, sonst den Wert NIL.

Aufgabe:
- Programm in Pseudocode für die lineare Suche, die eine Sequenz nach v durchsucht.
- Beweis der Korrektheit unter Verwendung der Schleifeninvariante</task>

Hallo!

Für die Aufgabe habe ich den folgenden Pseudocode erstellt:

Suche(A,v)
   i <- 1
   j <- 0

   while j=0 und i <= länge[A]
     do  if(A[i] = v)
           j <- 1
         i <- i+1

   if(j != 0)
     return i-1
   else
     return NIL

Was ist hier wohl die Schleifeninvariante? Der Vergleich if(A[i] = v) und der wert j, der anzeigen soll, ob v in A gefunden wurde?

Und wenn ja, ist folgender Beweis der Korrektheit richtig?:

Initialisierung:

Vor der ersten Iteration der while-Schleife ist der Wert der Laufvariable i = 1.
Die Variable j hat zu diesem Zeitpunkt den Wert 0, dh. der Wert v ist trivialer Weise in A noch nicht gefunden worden, da ja schließlich kein Vergleich stattfand.

Fotsezung:

Der Ausführungsblock der while-Schleife arbeitet so, dass v jeweils mit A[i+1], A[i+2], A[i+3] usw verglichen wird, bis ein A[k] aus A = <a1, a2, ... an> gefunden wird, für das gilt v = A[k].

Terminierung:

Die Schleife endet, sobald ein A[i] aus A gefunden worden ist, für das gilt: A[i] = v. Ist dies der Fall, so nimmt die Var. j den Wert 1 an.
Der gesuchte Index ist in dem Fall dann i-1.

Die Schleife endet aber auch, wenn kein A[i] gefunden worden ist, für das gilt: A[i] = v, und zwar dann, wenn i = n + 1. In diesem Fall bleibt j = 0.

Was sagt ihr dazu? - Bin für jede Kritik dankbar.

Eine Schleifeninvariante am Beginn des Schleifenrumpfes wäre: "v kommt nicht in A[0],...,A[i] vor."

Eine andere ist: 1 <= i <= Länge(A)

und auch: j == 0

(die beiden letzten sind natürlich trivial)

bzw. "v kommt nicht in A[1],...,A[i] vor", du zählst im Pseudocode ja ungewöhnlicherweise ab 1 hoch, nicht ab 0.

Heinzelotto

u_ser-l schrieb:

Eine Schleifeninvariante am Beginn des Schleifenrumpfes wäre: "v kommt nicht in A[0],...,A[i] vor."

Eine andere ist: 1 <= i <= Länge(A)

und auch: j == 0

(die beiden letzten sind natürlich trivial)

nicht ganz, die Invariante muss auch nach Beendigung der Schleife gelten.
Eine mögliche Invariante wäre also z.B. "v kommt nicht vor von A[1] bis A[i]-2" (minus zwei, weil in dem Fall, dass v erkannt wird, i noch um 1 erhöht wird).

PS: Die Arrayindizes sind aber komisch

Heinzelotto schrieb:

nicht ganz, die Invariante muss auch nach Beendigung der Schleife gelten.

muß sie nicht. Eine Schleifeninvariante an einem bestimmten Punkt innerhalb des Schleifenrumpfes muß in jedem Durchlauf gültig sein, unabhängig von der Zahl der Durchläufe - mehr nicht.

Heinzelotto

Wikipedia schrieb:

Beim Korrektheitsbeweis für einen Algorithmus mittels einer Schleifeninvariante ist zu zeigen, dass die Schleifeninvariante bei Initialisierung, Aufrechterhaltung und Beendigung der Schleife eingehalten wird.

In der Vorlesung haben wir es auch so gelernt (was natürlich nicht heißt, dass ich mich deshalb nicht eines Besseren belehren lasse ).

Oder habe ich irgendetwas übersehen (evtl. das "eine Schleifeninvariante an einem bestimmten Punkt")?

Jester

Man kann die Schleifeninvariante ja leicht aufbohren, dass sie auch den Fall, dass die Schleife terminiert mit abdeckt.

j=0,v kommt nicht in A[1],...,A[i] vor ODER j=1, v=A[i]

Heinzelotto schrieb:

Wikipedia schrieb:

[...] ist zu zeigen, dass die Schleifeninvariante bei Initialisierung, Aufrechterhaltung und Beendigung der Schleife eingehalten wird.

dann nimm doch Jester's Invariante - ich finde den Korrektheitsbeweis einfacher, wenn man die Invariante am Beginn des Schleifenrumpfes betrachtet, welche nach dem Aussprung natürlich nicht mehr gilt. Wenn ihr es in der Vorlesung anders macht, will ich dich nicht verwirren.