| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/sortPPPP/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 1 kB |
|
Quelle mergesort.vdmpp Sprache: VDM |
|||||||||
|
\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.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28