<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">Verifizieren: Beispiel Heapsort (?), 

sortiert \verb|a [1 .. a.length - 1]|
\begin{verbatim}
static void heapsort (double a []) {
    for (int i=2; i &lt; a.length; i++) {
        up (a, i);
    }
    for (int i=a.length - 1; i&gt;1; i--) {
        swap (a, 1, i);
        down (a, i);
    }
}
\end{verbatim}

prüfe, daß \verb|a[1 .. n-1]| heap-geordnet ist:
\begin{verbatim}
static void check (double a [], int n) {
    for (int i = 2; i&lt;n; i++) {
        assertTrue ("heap", a[parent(i)] &gt;= a[i]);
    }
}
\end{verbatim}

füge \verb|a[i]| in Heap \verb|a [1 .. i-1]| ein:
\begin{verbatim}
static void up (double a [], int i) {
    check (a, i); // vorbedingung
    while (i &gt; 1) {
        int j = parent (i);
        if (a[j] &lt; a[i]) {
            swap (a, j, i);
        }
        i = j;
    }
    check (a, i+1); // nachbedingung
}
\end{verbatim}
Zum Beweis (Schleifen-Invariante) wird abgeschwächte Bedingung 
\verb|check (a, n, j)| benutzt:
\verb|a[1 .. n-1]| ist \glqq eigentlich\grqq\ heap-geordnet, 
außer bei \verb|j|. (Genauer?)


Repariere Heap: \verb|a[2 .. n-1]| ist heap-geordnet,
aber Wert bei \verb|a[1]| ist möglicherweise falsch.
\begin{verbatim}
static void down (double a [], int n) { ... }
\end{verbatim}


</pre></body></html>