PUBS: A Practical Upper Bounds Solver
```
(* * * * * * * * * * *
* Resource Aware ML *
* * * * * * * * * * *
* File:
*   mergesort.raml
*
* Author:
*   Jan Hoffmann (2009)
*
* Resource Bound:
*   O(n^2)
*
* Description:
*   An implementation of the well known sorting algorithm mergesort.
*   This implementation deallocates the input list.  Copy the list before
*   if you want to use the unsorted list later.
*
*   It is suprising that the function mergesort can be analysed.  The
*   type of the function looks like the result of a bug on the first
*   view.  But it is correct.  The function mergesort is a nice
*   example of a type that might be hard to find without type
*   inference.
*
*   There is also an out commented buggy version of mergesort
*   (mergesortBuggy) that does not terminate and consumes an infinite
*   ammount of heap-space and time.  Thus our analysis does not work
*   for mergesortBuggy.  (Note that it is no general problem for our
*   analysis if a function does not terminate.  For example f(x) =
*   f(x) consumes no heap-space and can be analysed with the
*   heap-space metric.)
*)

(*
eq(mergeSort(N),1,[],[N =< 1]).
eq(mergeSort(N),1,[msplit(N), mergeSort(L1),mergeSort(L2),merge(L1,L2)],[N>=2,L1>=0,L2>=0,2*L1 =< N+1,2*L2=< N]).

eq(out2_msplit(N),0,[],[N=0]).
eq(out2_msplit(N),0,[],[N=1]).
eq(out2_msplit(N),1,[out2_msplit(Np)],[N>=2,Np = N-2]).

eq(out1_msplit(N),0,[],[N=0]).
eq(out1_msplit(N),1,[],[N=1]).
eq(out1_msplit(N),1,[out1_msplit(Np)],[N>=2,Np = N-2]).

eq(msplit(N),1,[],[N=0]).
eq(msplit(N),1,[],[N=1]).
eq(msplit(N),1,[msplit(Np)],[N>=2,Np = N-2]).

eq(merge(N1,N2),1,[],[N1=0]).
eq(merge(N1,N2),1,[],[N2=0]).
eq(merge(N1,N2),1,[merge(N1p,N2)],[N1>=1,N2>=1,N1p=N1-1]).
eq(merge(N1,N2),1,[merge(N1,N2p)],[N1>=1,N2>=1,N2p=N2-1]).

*)

mergesort: L(int) -> L(int)
(* mergesort as it is implemented in textbooks *)

mergesort l =  let _=tick(1) in
match l with
| nil -> nil
| (x1::xs) -> match xs with
| nil       -> x1::nil
| (x2::xs') -> let (l1,l2) = msplit (x1::x2::xs') in
merge (mergesort l1, mergesort l2);

msplit : L(int) -> (L(int),L(int))

msplit l =  let _=tick(1) in
matchD l with
| nil -> (nil,nil)
| (x1::xs) -> matchD xs with
| nil -> ([x1],nil)
| (x2::xs') -> let (l1,l2) = msplit xs' in
(x1::l1,x2::l2);

merge : (L(int),L(int)) -> L(int)

merge (l1,l2) = let _=tick(1) in
matchD l1 with
| nil -> l2
| (x::xs) -> matchD l2 with
| nil -> (x::xs)
| (y::ys) -> if x

|
Home
|
Solver
|
Examples

|
Help
|