[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 sort
enrich sorted with
   predicates 
      inv-outer : array × array × nat × (elem × elem → bool);
      inv-inner : array × array × nat × nat × (elem × elem → bool);
   procedures 
      sort#  (elem × elem → bool) : array nonfunctional;
   
   axioms 
      inv-outer
      :  ⊦ inv-outer(ar, ar0, n, ⊑) ↔ ¬ ¬ (n ≤ # ar ∧ ar .elems = ar0 .elems ∧ sorted(ar, 0, n, ⊑) ∧ reflexive(⊑) ∧ transitive(⊑) ∧ total(⊑));
      used for : ls;
       
      inv-inner
      : ⊦ 
          inv-inner(ar, ar0, n, m, ⊑)
        ↔ ¬ ¬ (  ar .elems = ar0 .elems ∧ n < # ar ∧ m ≤ n ∧ sorted(ar, 0, m, ⊑) ∧ sorted(ar, m, n + 1, ⊑) ∧ (m ≠ 0 ∧ m < n → ⊑(ar[m - 1], ar[m + 1]))
               ∧ reflexive(⊑) ∧ transitive(⊑) ∧ total(⊑));
      used for : ls;
       
declaration 
   sort
   : sort# (⊑; ar)
       { 
          let n = 0
          in while n < # ar
             do { 
                   let m = n in while m > 0 ∧ ¬ ⊑(ar[m - 1], ar[m]) do { 
                                                                          ar := ar[m, ar[m - 1]][m - 1, ar[m]] ; m := m - 1
                                                                       } ; n := n + 1
                }
       };
end enrich