[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification BubbleSort
enrich
   oarray-sort
, 
   gen-tord-min-max

with
   procedures bubblesort#  : array(tord) nonfunctional ;
   variables 
       ar : array(tord);
       AR : array(tord) flexible;
       n : nat;
       r : nat;
       N : nat flexible;
       R : nat flexible;
   
   
   declarations 
      bubblesort: 
      bubblesort#(; AR)
      {let R = # AR, R0 = 0, N = 0
       in while R > 1
          do {/* invariant perm(AR`, AR) ∧ ordered≤(restn(R, AR)) ∧ R ≤ # AR ∧ (R ≠ # AR → all≤(AR, 0, R, AR[R])) wfbound R */; 
              R0 := 0, N := 1; 
              while N < R
              do {/* invariant   perm(AR`, AR) ∧ ordered≤(restn(R, AR)) ∧ R ≠ 0 ∧ R ≠ 1 ∧ R ≤ # AR ∧ (R ≠ # AR → all≤(AR, 0, R, AR[R]))
                               ∧ all≤(AR, 0, R0, AR[R0]) ∧ R0 < N ∧ N ≠ 0 ∧ N ≤ R ∧ ordered≤(firstn(N - R0, restn(R0, AR)))
                     wfbound R - N */; 
                  if AR[N] < AR[N - 1] then {AR := AR[N, AR[N - 1]][N - 1, AR[N]]; R0 := N}; N := N + 1}; 
              R := R0}
      };
      
      
   
   
end enrich