Specification finddup

[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,

enrich array
 with
   
   procedures 
      FINDDUP#  array : nat × nat nonfunctional;
      FINDDUPSND#  array × elem : nat × nat nonfunctional;
   variables 
      bv : bool; 
      m0 : nat; 
declaration 
   FINDDUP
   : FINDDUP# (ar; m0, n0)
       { 
          let m = 0, bv = false
          in while m < # ar ∧ ¬ bv
             do { 
                   let n = m + 1 in while n < # ar ∧ ¬ bv do if ar[m] = ar[n]
                                                             then m0 := m, n0 := n, bv := true
                                                             else n := n + 1 ; m := m + 1
                }
       };
   FINDDUPSND
   : FINDDUPSND# (ar, a; m0, n0)
       { 
          let m = 0, bv = false
          in while m < # ar ∧ ¬ bv
             do { 
                   let n = m + 1 in while n < # ar ∧ ¬ bv do if ar[m] = ar[n] ∧ ar[m] ≠ a
                                                             then m0 := m, n0 := n, bv := true
                                                             else n := n + 1 ; 
                   m := m + 1
                }
       };
   
end enrich