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

Korrektheit von Quicksort

Aufgabe

1. Programmieren Sie Quicksort für beliebig lange Felder beliegigen Typs 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) → X] darstellen. Dabei ist X ein Typparameter, der für den Typ der Feldelemente steht.

• Um sortieren zu können muss man eine Ordnungsrelation auf X annehmen. Das kann man in PVS zum Beispiel mit Hilfe zweier Theorieparameter X : Type, ≤: (preorder?[X]) tun.