[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 array-splice
enrich
   array-copy
, 
   min-max
with
   

   
   constants  zero : elem;
              empty : elem;
   functions  mkzarray : nat → array;
             comment: create a zero-filled array of given length;
              mkemparray : nat → array;
             comment: create a empty-filled array of given length;
              splice : array × nat × array × nat × nat → array;
             comment: splice(ar0, n0, ar1, n1, m) copies m elements from ar0 from offset n0
         into ar1 starting from position n1, possibly extending the array and filling gaps with zero;
              resize : array × nat → array;
             comment: resize(ar, n) resizes ar to length n by trunctation or extension with zero;
              . + . : array × array → array;
             comment: appends two arrays;
   predicates  range= : array × nat × array × nat × nat;
              comment: range=(ar0,n0,ar1,n1,m) asserts that the range [n0..n0+m[ of ar0 equals [n1..n1+m[ of ar1
         and that all both ranges are within the array;
   
   
   
   

   

   axioms zarray :  ⊦ mkzarray(n) = fill(mkarray(n), zero);
          used for: ls;
          emparray :  ⊦ mkemparray(n) = fill(mkarray(n), empty);
          used for: ls;
          splice-copy :  ⊦ n1 + m ≤ # ar1 ∧ m ≠ 0 → splice(ar0, n0, ar1, n1, m) = copy(ar0, n0, ar1, n1, m);
          used for: s, ls;
          splice-resize :  ⊦ # ar1 < n1 + m ∧ m ≠ 0 → splice(ar0, n0, ar1, n1, m) = copy(ar0, n0, resize(ar1, n1 + m), n1, m);
          used for: s, ls;
          splice-0 :  ⊦ splice(ar0, n0, ar1, n1, 0) = ar1;
          used for: s, ls;
          resize-len :  ⊦ # resize(ar, n) = n;
          used for: s, ls;
          resize-at :  ⊦ m < n → resize(ar, n)[m] = (# ar ≤ m ∧ m < n ⊃ zero;ar[m]);
          used for: s, ls;
          range-eq-0 :  ⊦ range=(ar0, n0, ar1, n1, 0) ↔ n0 ≤ # ar0 ∧ n1 ≤ # ar1;
          used for: ws, lws;
          range-eq-rec :  ⊦ range=(ar0, n0, ar1, n1, m + 1) ↔ ar0[n0] = ar1[n1] ∧ range=(ar0, n0 + 1, ar1, n1 + 1, m);
          used for: lws;
          append :  ⊦ ar0 + ar1 = copy(ar1, 0, resize(ar0, # ar0 + # ar1), # ar0, # ar1);

   

   
end enrich