Merge sort as in Sedgewick

Semi automatic

  • 2 lemmas to be proved in Coq
  • see how to improve ?

    module MergeSort
    
      use import int.Int
      use import int.EuclideanDivision
      use import int.Div2
      use import ref.Ref
      use import array.Array
      use import array.IntArraySorted
      use import array.ArrayPermut
      use import array.ArrayEq
      use map.Map as M
      clone map.MapSorted as N with type elt = int, predicate le = (<=)
    
      predicate map_eq_sub_rev_offset (a1 a2: M.map int int) (l u: int) (offset: int) =
        forall i: int. l <= i < u -> M.get a1 i = M.get a2 (offset + l + u - 1 - i)
    
      predicate array_eq_sub_rev_offset (a1 a2: array int) (l u: int) (offset: int) =
         map_eq_sub_rev_offset a1.elts a2.elts l u offset
    
      predicate map_dsorted_sub (a: M.map int int) (l u: int) =
        forall i1 i2 : int. l <= i1 <= i2 < u -> M.get a i2 <= M.get a i1
    
      predicate dsorted_sub (a: array int) (l u: int) =
        map_dsorted_sub a.elts l u
    
      predicate map_bitonic_sub (a: M.map int int) (l u: int) =  l < u ->
        exists i: int. l <= i <= u /\ N.sorted_sub a l i /\ map_dsorted_sub a i u
    
      predicate bitonic (a: array int) (l u: int) =
        map_bitonic_sub a.elts l u
    
      lemma map_bitonic_incr : forall a: M.map int int, l u: int.
         map_bitonic_sub a l u -> map_bitonic_sub a (l+1) u
    
      lemma map_bitonic_decr : forall a: M.map int int, l u: int.
         map_bitonic_sub a l u -> map_bitonic_sub a l (u-1)
    
      predicate modified_inside (a1 a2: array int) (l u: int) =
        (Array.length a1 = Array.length a2) /\
        array_eq_sub a1 a2 0 l /\ array_eq_sub a1 a2 u (Array.length a1)
    
      let rec mergesort1 (a b: array int) (lo hi: int) =
        requires {Array.length a = Array.length b /\
                  0 <= lo <= (Array.length a) /\ 0 <= hi <= (Array.length a) }
        ensures { sorted_sub a lo hi /\ modified_inside (old a) a lo hi }
      if lo + 1 < hi then
      let m = div (lo+hi) 2 in
        assert{ lo < m < hi};
        mergesort1 a b lo m;
    'L2: mergesort1 a b m hi;
        assert { array_eq_sub (at a 'L2) a lo m};
        for i = lo to m-1 do
          invariant { array_eq_sub b a lo i}
          b[i] <- a[i]
          done;
        assert{ array_eq_sub a b lo m};
        assert{ sorted_sub b lo m};
        for j = m to hi-1 do
          invariant { array_eq_sub_rev_offset b a m j (hi - j)}
          invariant { array_eq_sub a b lo m}
          b[j] <- a[m + hi - 1 - j]
          done;
        assert{ array_eq_sub a b lo m};
        assert{ sorted_sub b lo m};
        assert{ array_eq_sub_rev_offset b a m hi 0};
        assert{ dsorted_sub b m hi};
    'L4: let i = ref lo in
        let j = ref hi in
        for k = lo to hi-1 do
          invariant{ lo <= !i < hi /\ lo <= !j <= hi}
          invariant{ k = !i + hi - !j}
          invariant{ sorted_sub a lo k }
          invariant{ forall k1 k2: int. lo <= k1 < k -> !i <= k2 < !j -> a[k1] <= b[k2] }
          invariant{ bitonic b !i !j }
          invariant{ modified_inside a (at a 'L4) lo hi }
          assert { !i < !j };
          if b[!i] < b[!j - 1] then
            begin a[k] <- b[!i]; i := !i + 1 end
          else
            begin j := !j - 1; a[k] <- b[!j] end
        done
    
      let mergesort (a: array int) =
        ensures { sorted a }
      let n = Array.length a in
      let b = Array.make n 0 in
        mergesort1 a b 0 n
    
    end
    

  • Generated by why3doc 0.85