Insertion sort in lists

  • fully automatic with help of CVC3
  • does not work without permut in insert post-cond
  • permut could be weakened to subset ?

    module InsertionSortList
      use import int.Int
      use import list.List
      use import list.Mem
      use import list.SortedInt
      use import list.Permut
    let rec insert x l
        requires { sorted l }
        ensures { sorted result /\ permut result (Cons x l) }
     =  match l with
        | Nil -> Cons x Nil
        | Cons y l' -> if x <= y then Cons x l else Cons y (insert x l')
    let rec insertionSort l
        ensures {sorted result}
     =  match l with
        | Nil -> Nil
        | Cons x l' -> insert x (insertionSort l')

  • Generated by why3doc 0.85