Quelle  mergesort.vdmpp

\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}