|
/**
* Implements a polymorphic quicksort for arbitrary types with a less function.
*/
class Sort
functions
equals[@T]: @T * @T * (@T * @T -> bool) -> bool
equals(a, b, less) ==
not less(a, b) and not less(b, a);
public sort[@T]: seq of @T * (@T * @T -> bool) -> seq of @T
sort(l, less) ==
cases l:
[] -> [],
[x] -> [x],
[x, y] -> if less(y, x)
then [y, x]
else [x, y], -- NB, stable for equality
-^[x]^- -> sort[@T]([y | y in seq l & less(y, x)], less) ^
[y | y in seq l & equals[@T](y, x, less) ] ^
sort[@T]([y | y in seq l & less(x, y)], less)
end
post bagOf[@T](l) = bagOf[@T](RESULT) and -- Permutation
forall i in set {1, ..., len RESULT - 1} &
not less(RESULT(i+1), RESULT(i)) -- Sorted!
measure len l; -- Strictly decreasing
bagOf[@T]: seq of @T -> map @T to nat
bagOf(s) ==
{ i |-> occurs[@T](i, s) | i in set elems s }
post dom RESULT = elems s and sizeOfBag[@T](RESULT) = len s;
sizeOfBag[@T]: map @T to nat -> nat
sizeOfBag(b) ==
if b = {|->}
then 0
else let e in set dom b in b(e) + sizeOfBag[@T]({e} <-: b)
measure card dom b; -- Strictly decreasing
occurs[@T]: @T * seq of @T -> nat
occurs(e, s) ==
if s = [] then 0
else (if e = hd s then 1 else 0) + occurs[@T](e, tl s)
measure len s; -- Strictly decreasing
end Sort
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
