Selection sort as in Sedgewick

Fully automatic

  • with use of swap
  • without swap, one should add assert{ permut a (a at 'L1) } (L1 at end of inner loop)

    module SelectionSort
    
     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 selection_sort (a: array int) =
        ensures { permut_all (old a) a }
    'L:
        for i = 0 to length a - 1 do
          invariant { permut_all (at a 'L) a }
          let min = ref i in
          for j = i + 1 to length a - 1 do
            invariant { i <= !min < j }
            if a[j] < a[!min] then min := j
          done;
          if !min <> i then swap a !min i
        done
    
    end
    

  • Generated by why3doc 0.85