[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 lrs-ops
enrich suffix-array-ops
 , 
       lrs with
   predicates 
      inv : nat × nat × nat × array × suffixarray;
   procedures 
      lrs#  array : nat × nat nondeterministic;
   variables 
      m1, m2 : nat; 
   
   axioms 
      inv
      : ⊦ 
          inv(n, m0, m1, ar, sar)
        ↔ ¬ ¬ (  valid(sar, ar) ∧ # ar ≠ 0 ∧ n ≤ # ar ∧ n ≠ 0
               ∧ (∃ m2. m2 ≤ # ar ∧ rs(ar, m1, m2, m0) ∧ (∀ n0, n1. n1 + 1 < n ∧ rs(ar, sar[n1 + 1], sar[n1], n0) → n0 ≤ m0)));
      used for : ls;
       
declaration 
   lrs
   : lrs# (ar; m0, m1)
       { 
          m0 := 0 ; 
          m1 := 0 ; 
          let sar = [?]
          in { 
                create_suffixarray#(ar; sar) ; 
                let n = 1
                in while n < # ar do let n0 = [?] in { 
                                                        lcp#(ar, sar[n], sar[n - 1]; n0) ; if n0 > m0
                                                        then { 
                                                                m0 := n0 ; m1 := sar[n]
                                                             } ; n := n + 1
                                                     }
             }
       };
end enrich