Korrektheit eines Algorithmus

[SvenInfo12]

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.

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]

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

 

[SvenInfo12]

Tut mir leid. Ich werde nächstes mal darauf besser achten. Hast du vllt eine Idee zu meinem Problem?

 

[ComFreek]

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:

∀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?

Spoiler

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