Specification fsarray-copy

[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
   fsarray
with
   functions 
       fill : FSArray[A] × A → FSArray[A];
      comment: fill complete array;
   
   predicates 
       id○ : FSArray[A] × FSArray[A] × Nat;
      comment: id○(ar0, ar1, n) is true if all elements except those at offset n are equal;
       id○ : FSArray[A] × FSArray[A] × Nat × Nat;
      comment: id○(ar0, ar1, n, m) is true if all elements except those at indices [n, n + m[ are equal;
       cmp : FSArray[A] × A;
   
   variables 
       m : Nat;
       n : Nat;
       ar : FSArray[A];
       a : A;
   
   partial functions 
       fill : FSArray[A] × A × Nat × Nat → FSArray[A] with λ ar, a, n, m. n + m ≤ size;
      comment: fill(ar, a, offset, len) sets len indices from offset (inclusive) to a;
       copy : FSArray[A] × Nat × FSArray[A] × Nat × Nat → FSArray[A] with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ size;
      comment: copy(ar, m, ar0, m0, n) copy from ar at offset m into ar0 at offset m0
                   n elements and return new ar0;
   
   partial predicates 
       cmp : FSArray[A] × Nat × FSArray[A] × Nat × Nat with λ ar, m, ar0, m0, n. m + n ≤ size ∧ m0 + n ≤ size;
      comment: cmp(ar, m, ar0, m0, n) compares n elements of ar from offset m with ar0
                    from offset m0;
       cmp : FSArray[A] × A × Nat × Nat with λ ar, a, m, n. m + n ≤ size;
      comment: cmp(ar, a, m, n) is true if all elements in the range at offset m 
                    with length n are equal to a;
       idrange : FSArray[A] × Nat × Nat with λ ar, m, n. m + n ≤ size;
      comment: idrange(ar, m, n) is true if all elements
                    in the range at offset m with length n are equal;
   
   axioms 
      Fill-zero: fill(ar, a, m, 0) = ar;
      used for: s, ls;
      
      Fill-succ: fill(ar, a, m, n + 1) = fill(ar, a, m, n)(m + n := a);
      used for: s, ls;
      
      Fill-all: fill(ar, a) = fill(ar, a, 0, size);
      used for: ls;
      
      Copy-zero: copy(ar, m, ar0, m0, 0) = ar0;
      used for: s, ls;
      
      Copy-succ: copy(ar, m, ar0, m0, n + 1) = copy(ar, m, ar0, m0, n)(m0 + n := ar(m + n));
      used for: ls;
      
      Compare: cmp(ar, m, ar0, m0, n) ↔ (∀ n0. n0 < n → ar(m + n0) = ar0(m0 + n0));
      
      Cmp: cmp(ar, a) ↔ (∀ n. n < size → ar(n) = a);
      used for: ls;
      
      Cmp-elem: cmp(ar, a, m, n) ↔ (∀ n0. n0 < n → ar(m + n0) = a);
      
      Idrange: idrange(ar, m, n) ↔ (∀ n0. n0 < n → ar(m + n0) = ar(m));
      
      Idexcept: id○(ar0, ar1, n) ↔ (∀ m. m < # ar0 ∧ m ≠ n → ar0(m) = ar1(m));
      used for: ls;
      
      Idexcept-n: id○(ar0, ar1, m, n) ↔ m + n ≤ size ∧ (∀ m0. (m0 < m ∨ m + n ≤ m0) ∧ m0 < # ar0 → ar0(m0) = ar1(m0));
      used for: ls;
   
   
end enrich