Mergesort on lists

  • fully automatic with help of CVC3, Eprover, Alt-Ergo, Z3 !!

    module MergeSortList
    
      use import int.Int
      use import list.List
      use import list.Length
      use import list.SortedInt
      use import list.Append
      use import list.Permut
    
     let rec split (l : list int)
     ensures { let (l1, l2) = result in permut l (l1 ++ l2)}
      = match l with
        | Nil -> (Nil, Nil)
        | Cons x Nil -> ((Cons x Nil) , Nil)
        | Cons x (Cons y l') -> let (xs, ys) = split l' in ((Cons x xs), (Cons y ys))
        end
    
     let rec merge l1 l2
      ensures { permut result (l1 ++ l2)}
      = match l1, l2 with
        | Nil, _ -> l2
        | _, Nil -> l1
        | Cons x1 r1, Cons x2 r2 ->
           if x1 <= x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2)
        end
    
     let rec mergesort l
     ensures {permut result l}
      = match l with
        | Nil | Cons _ Nil -> l
        | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2)
        end
    
    end
    

  • Generated by why3doc 0.85