|
\section{MergeSort}
\begin{vdm_al}
class MergeSort is subclass of Sorter
operations
public Sort: seq of int ==> seq of int
Sort(l) ==
return MergeSorter(l)
functions
MergeSorter: seq of real -> seq of real
MergeSorter(l) ==
cases l:
[] -> l,
[e] -> l,
others -> let l1^l2 in set {l} be st abs (len l1 - len l2) < 2
in
let l_l = MergeSorter(l1),
l_r = MergeSorter(l2) in
Merge(l_l, l_r)
end
measure Len;
Len: seq of real -> nat
Len(list) ==
len list;
\end{vdm_al}
Although the \texttt{Merge} function takes sequence of integers it has on purpose been
limited by the pre-condition "artificially" to only work for natural numbers in order to
illustrate how the debugger can catch such pre-condition violations when called with
negative numbers.
\begin{vdm_al}
Merge: seq of int * seq of int -> seq of int
Merge(l1,l2) ==
cases mk_(l1,l2):
mk_([],l),mk_(l,[]) -> l,
others -> if hd l1 <= hd l2 then
[hd l1] ^ Merge(tl l1, l2)
else
[hd l2] ^ Merge(l1, tl l2)
end
pre forall i in set inds l1 & l1(i) >= 0 and
forall i in set inds l2 & l2(i) >= 0
measure Len;
Len: seq of int * seq of int -> nat
Len(list1,list2) ==
len list1 + len list2;
end MergeSort
\end{vdm_al}
¤ Dauer der Verarbeitung: 0.19 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.
|
