The Scheme source file
sort.ss
contains two recursive list-sorting programs,
MergeSort
and
QuickSort.
Run these sorting functions on a few lists of numbers to confirm that they
work.
(Optional but recommended) Write out correctness proofs for the two functions
by hand.
Translate these function definitions to PVS, or if you prefer,
use the translations in sort.pvs
Correctness properties
'ordered?'
and
'permutation?'
are the same as those used for list
BubbleSort
in Homework Assignment 7.
In PVS, prove that
MergeSort
and
QuickSort
are correct.
Suggestion: The
'ordered?'
property is easier to
prove than the
'permutation?'
propery, so work through
'ordered?'
first.