Korrektheit eines Algorithmus


#1
Hallo, ich will die Korrektheit von folgendem Algorithmus zeigen. Es geht um die Medianbestimmung eines Feldes A mit n Zahlen unter Verwendung der Partition-Methode von Quicksort.

Java:
n=[n+1/2]
l=1
r=n
while(r<=n) do
    q=partition(A,l,r)
    if q=m then
        return A[q]
    else
        if q>m then
            r=q-1
        else
            l=q+1
Nach Anwendung der Methode Partition auf den Bereich l bis r stehen von l bis q alle Elemente kleiner als A[q] bzw. in q+1 bis r alle Elemente größer als A[q].

Brauche ich für den Korrektheitsbeweis eine Invariante?
Ich komme leider nicht weiter. Ein kleiner Tipp würde schon sehr helfen:)
 

zerix

Hausmeister
Moderator
#2
Hey,

warum stellst du die Fragen eigentlich immer im Java Forum? Sinnvoller wäre es im Coders-Talk, da die Probleme selbst sprachunabhängig sind. Ich werde es somit verschieben und dich bitten doch nächstes mal direkt dort dein Thema zu erstellen. :)

Viele Grüße
Sascha
 

ComFreek

Mod | @comfreek
Moderator
#4
Wo kommt das m im Algorithmus her? Ah, in der ersten Zeile sollte wohl m zugewiesen werden.

Ich sehe gerade nicht, warum der Algorithmus überhaupt korrekt ist. Angenommen ich habe das Array [0, 3, 2, 4, 5] und die erste Partitionierung ist ein No-op und liefert einfach den Index der 5 zurück. Dann würde ich ja in das linke Teilarray [0, 3, 2, 4] gehen und weitermachen.

Ah, du verändest das m eben nicht. Dadurch wird er korrekt. Lass mich nachdenken.

Versuche es mal mit dieser Invariante:
Code:
∀i≤q: A[i] ≤ A[q]   ∧   ∀i≥q: A[i] ≥ A[q]
Damit (oder mit einer kleinen Variation) kannst du wahrscheinlich Korrektheit, aber nicht Termination zeigen. D.h., wenn der Algorithmus jemals aus dem while via der ersten IF-Bedingung rauskommt, dann hat er ein korrektes Ergebnis.
Damit aber das IF jemals zuschlägt, brauchst du eine weitere Bedingung. Kommst du drauf?

Code:
m ∈ [l, r]   ∧   ∀i≤q: A[i] ≤ A[q]   ∧   ∀i≥q: A[i] ≥ A[q]
 
Zuletzt bearbeitet:

Neue Beiträge