\section{DoSort}
\begin{vdm_al}
class DoSort is subclass of Sorter

operations

  public Sort: seq of int ==> seq of int
  Sort(l) ==
    return DoSorting(l)
 
functions

  DoSorting: seq of int -> seq of int
  DoSorting(l) ==
    if l = [] then
      []
    else
      let sorted = DoSorting (tl l) in
        InsertSorted (hd l, sorted)
  measure Len;

  InsertSorted: int * seq of int -> seq of int
  InsertSorted(i,l) ==
    cases true :
      (l = [])    -> [i],
      (i <= hd l) -> [i] ^ l,
      others      -> [hd l] ^ InsertSorted(i,tl l)
    end
  measure Len;

  Len: seq of int -> nat
  Len(list) ==
    len list;

  Len: int * seq of int -> nat
  Len(-,list) ==
    len list

end DoSort 
\end{vdm_al}