Insertion sort -- with swap

Fully automatic with Alt-Ergo

  • but needs 'permut' assert in inner loop !!

    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 swap (a: array int) (i: int) (j: int) =
        requires { 0 <= i < length a /\ 0 <= j < length a }
        ensures { exchange (old a) a i j }
       let v = a[i] in
        a[i] <- a[j];
        a[j] <- v
    
      let insertion_sort (a: array int) =
        ensures { sorted a /\ permut_all (old a) a }
    'L:
        for i = 1 to length a - 1 do
          invariant { sorted_sub a 0 i /\ permut_all (at a 'L) a }
          let j = ref i in
    'L1:
          while !j > 0 && a[!j - 1] > a[!j] do
            invariant { 0 <= !j <= i }
            invariant { permut_all (at a 'L) a}
            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 -> a[!j] < a[k] }
            variant { !j }
            swap a (!j-1) !j;
            assert { permut_all (at a 'L1) a } ;
            j := !j - 1
          done
        done
    
    end
    

  • Generated by why3doc 0.85