Specification array-fsarray

[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-copy, 
   fsarray-copy
with
   functions 
       . toArray : FSArray → Array;
      comment: returns array with of length 'size';
   
   variables 
       m : Nat;
       n : Nat;
       ar : Array;
       fsar : FSArray;
       a : Elem;
   
   partial functions 
       copy : Array × Nat × FSArray × Nat × Nat → FSArray with λ ar, m, fsar, m0, n. m + n ≤ # ar ∧ m0 + n ≤ size;
      comment: copy(ar, m, fsar, m0, n) copy from ar at offset m into fsar at offset m0
                   n elements and return new fsar;
       copy : FSArray × Nat × Array × Nat × Nat → Array with λ fsar, m, ar, m0, n. m + n ≤ size ∧ m0 + n ≤ # ar;
      comment: copy(fsar, m, ar, m0, n) copy from fsar at offset m into ar at offset m0
                   n elements and return new ar;
       subarray : FSArray × Nat × Nat → Array with λ fsar, m, n. m + n ≤ size;
      comment: subarray(fsar, m, n) returns subarray of ar from offset m with length n;
       . toFSArray : Array → FSArray with λ ar. # ar = size;
      comment: removes size field of array (requires #ar = size);
   
   partial predicates 
       cmp : FSArray × Nat × Array × Nat × Nat with λ fsar, m, ar, m0, n. m + n ≤ size ∧ m0 + n ≤ # ar;
      comment: cmp(ar, m, ar0, m0, n) compares n elements of ar from offset m with ar0
                    from offset m0;
   
   axioms 
      FSCopy-zero: copy(fsar, m, ar, m0, 0) = ar;
      used for: s, ls;
      
      FSCopy-succ: copy(fsar, m, ar, m0, n + 1) = copy(fsar, m, ar, m0, n)(m0 + n := ar(m + n));
      used for: ls;
      
      CopyFS-zero: copy(ar, m, fsar, m0, 0) = fsar;
      used for: s, ls;
      
      CopyFS-succ: copy(ar, m, fsar, m0, n + 1) = copy(ar, m, fsar, m0, n)(m0 + n := ar(m + n));
      used for: ls;
      
      Compare: cmp(fsar, m, ar, m0, n) ↔ (∀ n0. n0 < n → fsar(m + n0) = ar(m0 + n0));
      
      toArray-size: # fsar.toArray = size;
      used for: s, ls;
      
      toArray-get: n < size ⊦ fsar.toArray(n) = fsar(n);
      used for: s, ls;
      
      toFSArray-get: n < size ⊦ ar.toFSArray(n) = ar(n);
      used for: s, ls;
   
   
end enrich