Fragen zu Schleifeninvarianten

[der_kater]

Hallo Leute,

ich sitze grad hier und lerne Schleifeninvarianten. Ich habe hier einen Algorithmus, um aus einem Array von Integern die kleinste Zahl zu finden

min_array(a[n]) {

min <- a[0]

while(j < n) {

if(a[j] < min) {

min <- a[j]

}

j <- j + 1

}

}

So, nun möchte ich hierzu eine Schleifeninvariante erstellen. Wie fange ich am besten an? Ich habe keinen Plan wie ich anfangen soll bzw. wie ich sowas formal korrekt aufschreiben kann. Falls es irgendwo auch Links geben sollte, wo das gut erklärt wird, nur her damit. Ich steh gerade echt auf dem Schlauch...

[flashpixx]

also das hier hilft definitiv weiter (vor allem das Bsp) Schleifeninvariante ? Wikipedia

Kann man aber durch eigenständige Recherche auch selbst finden

Phil

[der_kater]

Den Text in Wikipedia hab ich mir schon durchgelesen, so isses ja nicht ...

Ist denn zum obigen Algorithmus das hier eine Schleifeninvariante: I(x) speichert den kleinsten Wert.

1) I(a[0]) = (min_array(a[0])) = a[0]

2) Annahme: I(a[j - 1]) = (min_array(a[0, ..., j - 1])) hat den Wert kleinsten Wert

3) Induktion: I(a[j]) = (Prüft, welcher Wert kleiner ist, a[j] oder min_array(a[0, ..., j - 1]) => min_array(a[0, ..., j])

4) Schluss: I(a[n]) = (min_array(a[0, ..., n]))

Kann man das denn so aufschreiben für den obigen Algorithmus oder gibt es noch eine bessere / andere Lösung?

[flashpixx]

Den Text in Wikipedia hab ich mir schon durchgelesen, so isses ja nicht ...

Dann lies doch einmal den Artikel genau

Als Schleifeninvariante werden Eigenschaften einer Schleife in einem Algorithmus bezeichnet, die zu einem bestimmten Punkt bei jedem Schleifendurchlauf gültig sind, unabhängig von der Zahl ihrer derzeitigen Durchläufe.

und überlege Dir, ob das bei Deiner Invariante zutreffend ist. Deine 2. Aussage I(a[j-1]) kann schon nicht stimmen, denn j ist zu Beginn == 0, somit ist a[j-1] nicht definiert und damit schlägt jeder Beweis fehl. Zusätzlich hast Du nicht j-1 im Code stehen, sondern j+1, d.h. Du musst Deinen Beweis schon anhand des Codes führen

Phil

[der_kater]

Deine 2. Aussage I(a[j-1]) kann schon nicht stimmen, denn j ist zu Beginn == 0, somit ist a[j-1] nicht definiert und damit schlägt jeder Beweis fehl.

Stimmt, daran hab ich nicht gedacht. D.h. ich änder das auf:

2) Annahme: I(a[j]) = (min_array(a[0, ..., j])) hat den Wert kleinsten Wert

3) Induktion: I(a[j + 1]) = (Prüft, welcher Wert kleiner ist, a[j + 1] oder min_array(a[0, ..., j]) => min_array(a[0, ..., j + 1])

Es ist doch kein Fehler, wenn ich noch dahinter schreibe, dass man prüft, ob j < n ist, quasi I(...) = (min_...) und j < n.

Ich denk mal dass ich dann beim Algorithmus nach der zweiten Zeile ein j <- 0 reinschieben muss...

Ein doch etwas schwierigeres Thema ...

[flashpixx]

Schau Dir bitte einmal Induktionsbeweise an, denn so würde ich Dir als Tutor den Beweis nicht durchgehen lassen!

Du musst den Beweis zu Beginn der Schleife benutzen, also für j==0.

Dann musst Du entsprechende der Induktion und des Codes zeigen, dass immer Deine Bedingung für ein j+1 gilt, wenn Du voraussetzt, dass j gilt und der dritte Schritt ist, Du musst zeigen, dass die Bedingung auch nach der Schleife also für j==n gilt und auch dass j == n wird

Wenn Du nämlich einen Fall auslässt, dann ist damit gezeigt, dass der Befehl irgendetwas macht, aber es ist nicht sicher gestellt, dass der Algorithmus terminiert. Der Beweis via Induktion für Schleifeninvarianten ist dafür gedacht zu zeigen, dass ein Codestück / Algorithmus bei einer gültigen Eingabe von Daten immer terminiert.

Nach Deinem Beweis kann ich das j > n wählen und damit habe ich in Deinem Verfahren schon ein Gegenbeispiel gefunden, dass Deinen Beweis widerlegt. Es geht hier nicht um "programmieren", sondern um eine mathematische formale Beweisführung

Phil