|
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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
