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 : LEMMANOT 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
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung:
(vorverarbeitet)
¤
