Mergesort on lists

  • fully automatic with help of CVC3, Eprover, Alt-Ergo, Z3 !!
  • permut needed to prove sorted in merge

    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
      requires { sorted l1 /\ sorted l2}
      ensures { sorted result /\ 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 { sorted result }
      = 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