Angewandte Softwareverifikation mit einem interaktiven Theorembeweiser Version 28. März 2011

Korrektheit von Heapsort

Heapsort ist etwas unbekannter als Quicksort, hat aber die gleiche Komplexität von O(n log(n)). Siehe http://www.iti.fh-flensburg.de/lang/algorithmen/sortieren/heap/heap.htm.

Aufgabe

1. Programmieren Sie Heapsort für beliebig lange Felder in Pvs als rekursive Funktion.

2. Beweisen Sie die Korrektheit der Sortierfunction.

Detaillierte Hinweise

• Ein Feld der Länge n kann man gut als Funktion [below(n) → nat] darstellen.

• Es ist ausreichend, den Algorithmus für Felder natürlicher Zahlen und die normale ”kleiner-gleich“ Relation zu formulieren und zu verifizieren.