Insertion sort as in Sedgewick

  • fully automatic (could be simpler with swap)

    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 { permut_all (old a) a }
    'L:
        for i = 1 to length a - 1 do
          invariant { permut_all (at a 'L) a }
    'L1:
          let v = a[i] in
          let j = ref i in
          while !j > 0 && a[!j - 1] > v do
            invariant { 0 <= !j <= i }
            invariant { permut_all (at a 'L1) a[!j <- v] }
    'L2:
            a[!j] <- a[!j - 1];
            assert { exchange (at a 'L2)[!j <- v] a[!j-1 <- v] (!j - 1) !j};
            j := !j - 1
          done;
          a[!j] <- v
        done
    
    end
    

  • Generated by why3doc 0.85