Insertion sort as in Sedgewick

  • fully automatic

    module InsertionSort
    
      use import int.Int
      use import ref.Ref
      use import array.Array
      use import array.IntArraySorted
      use import array.ArrayPermut
      use import array.ArrayEq
    
      let insertion_sort (a: array int) =
        ensures { sorted a }
        for i = 1 to length a - 1 do
          invariant { sorted_sub a 0 i }
          let v = a[i] in
          let j = ref i in
          while !j > 0 && a[!j - 1] > v do
            invariant { 0 <= !j <= i }
            invariant { forall k1 k2: int. 0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> a[k1] <= a[k2] }
            invariant { forall k: int. !j+1 <= k <= i -> v < a[k] }
            a[!j] <- a[!j - 1];
            j := !j - 1
          done;
          a[!j] <- v
        done
    
    end
    

  • Generated by why3doc 0.85