;;; ;;; See sort.pvs ;;; ;;; Bubble(j, l): RECURSIVE slist = ;;; CASES l OF ;;; null: cons(j, null), ;;; cons(k, tl): IF j <= k ;;; THEN cons(j, Bubble(k, tl)) ;;; ELSE cons(k, Bubble(j, tl)) ;;; ENDIF ;;; ENDCASES ;;; MEASURE l BY << ;;; ;;; BubbleSort(l): RECURSIVE slist = ;;; CASES l OF ;;; null: null, ;;; cons(k, tl): Bubble(k, BubbleSort(tl)) ;;; ENDCASES ;;; MEASURE l BY << ;;; (define Bubble (lambda (j l) (if (null? l) (cons j `()) (let ((k (car l)) (tl (cdr l))) (if (<= j k) (cons j (Bubble k tl)) (cons k (Bubble j tl))))))) (define BubbleSort (lambda (l) (if (null? l) `() (let ((k (car l)) (tl (cdr l))) (Bubble k (BubbleSort tl)))))) #| Test BubbleSort (Bubble 5 `(1 2 3 4 6)) (BubbleSort `(5 4 3 2 1 6)) |#