[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-col
enrich
   matrix-revops, 
   oarray-sort
, 
   gen-tord-min-max

with
   procedures psortcol# nat : matrix(tord) nonfunctional ;
   variables 
       mx : matrix(tord);
       MX : matrix(tord) flexible;
       N : nat flexible;
       R : nat flexible;
       C : nat flexible;
       ar : array(tord);
       n : nat;
       a : tord;
   
   
   theorems 
      psortcol-correct: 
      MX[c]c = mx[c]c, C = c, c < #c MX, #c MX = #c mx, #r MX = #r mx, #r mx ≠ 0, #c mx ≠ 0
      ⊦ ⟨: MX, C
        | (MX''[c]c = MX'[c]c ∧ #c MX'' = #c MX')
        , (MX' = MX[c, MX'[c]c]c ∧ #r MX' = #r MX)
        , (C = c ∧ #c MX = #c mx ∧ #r MX = #r mx)
        , psortcol#(C; MX)
        ⟩ (C = c ∧ perm(mx[C]c, MX[C]c) ∧ ordered≤(MX[C]c));
   
   declarations 
      psortcol: 
      psortcol#(C; MX)
      {let R = #r MX, R0 = 0, N = 0
       in while R > 1
          do {/* invariant perm((MX`)[C]c, MX[C]c) ∧ ordered≤(restn(R, MX[C]c)) ∧ R ≤ #r MX ∧ (R ≠ #r MX → all≤(MX[C]c, 0, R, MX[R, C]))
                 wfbound R */; 
              R0 := 0, N := 1; 
              while N < R
              do {/* invariant   perm((MX`)[C]c, MX[C]c) ∧ ordered≤(restn(R, MX[C]c)) ∧ R ≠ 0 ∧ R ≠ 1 ∧ R ≤ #r MX
                               ∧ (R ≠ #r MX → all≤(MX[C]c, 0, R, MX[R, C])) ∧ all≤(MX[C]c, 0, R0, MX[R0, C]) ∧ R0 < N ∧ N ≠ 0 ∧ N ≤ R
                               ∧ ordered≤(firstn(N - R0, restn(R0, MX[C]c)))
                     wfbound R - N */; 
                  if MX[N, C] < MX[N - 1, C] then {MX := MX[N - 1, C, MX[N, C]][N, C, MX[N - 1, C]]; R0 := N}; N := N + 1}; 
              R := R0}
      };
      
      
   
   
end enrich