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

Korrektheit von Bitonic Sort

Bitonic Sort ist ein etwas unbekannterer Sortieralgorithmus der Komplexität O(n log(n)^{2}). Das besondere an Bitonic Sort ist, dass die Anzahl zu vergleichenden Elemente unabhängig von den Daten sind. Bitonic Sort läßt sich deshalb in Hardware realisieren. Siehe http://www.iti.fh-flensburg.de/lang/algorithmen/sortieren/bitonic/bitonic.htm.

Aufgabe

1. Programmieren Sie Bitonic Sort 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.