Bubble sort as in Sedgewick

  • fully automatic (permut_sub necessary? )

    module BubbleSort
    
      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 bubble_sort (a: array int) =
        ensures { sorted a }
    'L:
        for i = length a downto 2 do
          invariant { sorted_sub a i (length a) }
          invariant { forall k: int. forall k': int. 0 <= k < i -> i <= k' < length a
              -> a[k] <= a[k'] }
    'L1:    for j = 1 to i-1 do
            invariant { forall k: int. 0 <= k < j-1 -> a[k] <= a[j-1] }
    	invariant { array_eq_sub (at a 'L1) a i (length a) }
            invariant { permut_sub (at a 'L1) a 0 i }
    'L2:
            if a[j-1] > a[j] then begin
              let t = a[j] in a[j] <- a[j-1]; a[j-1] <- t;
              assert { exchange (at a 'L2) a (j - 1) j }
            end
          done
        done
    
    end
    

  • Generated by why3doc 0.85