Bubble sort as in Sedgewick

  • fully automatic (why 2nd permut_sub assertion needed? )

    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 { permut_all (old a) a }
    'L:
        for i = length a downto 2 do
          invariant { permut_all (at a 'L) a }
    'L1:    for j = 1 to i-1 do
            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 };
              assert { permut_sub (at a 'L2) a 0 i }
            end
          done
        done
    
    end
    

  • Generated by why3doc 0.85