Quelle  bubblesort.pvs

bubblesort[N: posnat, T: TYPE, <= : (total_order?[T]) ]: THEORY
%----------------------------------------------------------------------------
% The bubblesort algorithm and its correctness.
%
% Author: Alfons Geser, National Institute of Aerospace, 2003
%----------------------------------------------------------------------------
BEGIN

  IMPORTING sort_inversions[N,T,<=]

  A: VAR [below(N) -> T]
  inv: VAR finite_set[index_pair]
  i,j,k: VAR below(N)
  x: VAR T

  epsilon_lem  : LEMMA NOT sorted?(A) &
                       (j = epsilon! j: j < N - 1 & NOT A(j) <= A(j+1)) =>
                              j < N - 1 & NOT A(j) <= A(j+1)

  bubblesort(A): RECURSIVE [below(N) -> T] =
                      IF sorted?(A) THEN A
                      ELSE
                        LET j = epsilon! j: j < N-1 & NOT A(j) <= A(j+1) IN
                        bubblesort(A o transpose(j,j+1))
                      ENDIF
                   MEASURE card(inversions(A))

  sorted_bubblesort: THEOREM sorted?(bubblesort(A))

END bubblesort