enrich
   array
with
   functions 
       fill : Array × Elem → Array;
      comment: fill complete array;
       resize : Array × Nat → Array;
      comment: resize the array. When enlarged, elements at new indices are unspecified;
   
   predicates 
       id○ : Array × Array × Nat;
      comment: id○(ar0, ar1, n) is true if all elements except those at offset n are equal;
       id○ : Array × Array × Nat × Nat;
      comment: id○(ar0, ar1, n, m) is true if all elements except those at indices [n, n + m[ are equal;
       cmp : Array × Elem;
   
   procedures moveAndFill# Nat × Nat × Nat × Elem : Array nonfunctional ;
              comment: moveAndFill#(m,m0,n,ar) works like ar := move(ar,m,m0,n), but fills elements that would be duplicated with a;
              copyAndFill# Nat × Nat × Nat × Elem : Array × Array nonfunctional ;
              comment: copyAndFill#(m,m0,n, ar, ar0) works like ar0 := copy(ar,m,ar0, m0,n), but fills the elements in ar that were copied with a;
   variables 
       m : Nat;
       n : Nat;
       ar : Array;
       a : Elem;
   
   partial functions 
       fill : Array × Elem × Nat × Nat → Array with λ ar, a, n, m. n + m ≤ # ar;
      comment: fill(ar, a, offset, len) sets len indices from offset (inclusive) to a;
       copy : Array × Nat × Array × Nat × Nat → Array with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0;
      comment: copy(ar, m, ar0, m0, n) copy from ar at offset m into ar0 at offset m0
                   n elements and return new ar0;
       subarray : Array × Nat × Nat → Array with λ ar, m, n. m + n ≤ # ar;
      comment: subarray(ar, m, n) returns subarray of ar from offset m with length n;
       shiftLeft : Array × Nat × Nat × Nat → Array with λ ar, m, n, n0. m + n ≤ # ar ∧ n0 ≤ m;
      comment: shiftLeft(ar, m, n, n0) moves the n elements starting at offset m by n0 to the left, should correspond to memmove(ar + m, ar + m - n0, n) in C;
       shiftRight : Array × Nat × Nat × Nat → Array with λ ar, m, n, n0. m + n + n0 ≤ # ar;
      comment: shiftRight(ar, m, n, n0) moves the n elements starting at offset m by n0 to the right, should correspond to memmove(ar + m, ar + m + n0, n) in C;
       rotateLeft : Array × Nat × Nat × Nat → Array with λ ar, m, n, n0. m + n ≤ # ar ∧ n0 ≤ m;
      comment: rotateLeft (ar, m, n, n0) moves the n elements starting at offset m by n0 to the left and moves the overwritten elements to m + n0;
       rotateRight : Array × Nat × Nat × Nat → Array with λ ar, m, n, n0. m + n + n0 ≤ # ar;
      comment: rotateRight: (ar, m, n, n0) moves the n elements starting at offset m by n0 to the right and moves the overwritten elements to m;
       move : Array × Nat × Nat × Nat → Array with λ ar, m, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar;
      comment: move(ar, m, m0, n) moves the n elements starting at offset m to the n elements starting at n0, should correspond to memmove(ar + m, ar + m0, n) in C;
   
   partial predicates 
       cmp : Array × Nat × Array × Nat × Nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0;
      comment: cmp(ar, m, ar0, m0, n) compares n elements of ar from offset m with ar0
                    from offset m0;
       cmp : Array × Elem × Nat × Nat with λ ar, a, m, n. m + n ≤ # ar;
      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 : Array × Nat × Nat with λ ar, m, n. m + n ≤ # ar;
      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, # ar);
      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;
      
      Subarray: subarray(ar, m, n) = copy(ar, m, mkarray(n), 0, 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 < # ar → 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) ↔ # ar0 = # ar1 ∧ (∀ m. m < # ar0 ∧ m ≠ n → ar0(m) = ar1(m));
      used for: ls;
      
      Idexcept-n: 
      id○(ar0, ar1, m, n) ↔ # ar0 = # ar1 ∧ m + n ≤ # ar0 ∧ (∀ m0. (m0 < m ∨ m + n ≤ m0) ∧ m0 < # ar0 → ar0(m0) = ar1(m0));
      used for: ls;
      
      shiftLeft: shiftLeft(ar, m, n, n0) = copy(ar, m, ar, m - n0, n);
      used for: ls;
      
      shiftRight: shiftRight(ar, m, n, n0) = copy(ar, m, ar, m + n0, n);
      used for: ls;
      
      move-right: m < m0 → move(ar, m, m0, n) = shiftRight(ar, m, n, m0 - m);
      
      move-left: m0 ≤ m → move(ar, m, m0, n) = shiftLeft(ar, m, n, m - m0);
      
      rotateLeft: rotateLeft(ar, m, n, n0) = copy(copy(copy(ar, 0, ar, 0, # ar), m - n0, ar, m - n0, n), m - n0 + n, ar, m - n0 + n, n0);
      used for: ls;
      
      rotateRight: rotateRight(ar, m, n, n0) = copy(copy(copy(ar, 0, ar, 0, # ar), m, ar, m + n, n0), m + n0, ar, m + n0, n);
      used for: ls;
      
      resize-size: # resize(ar, n) = n;
      used for: s, ls;
      
      resize-get: m < # ar ∧ m < n → resize(ar, n)(m) = ar(m);
      used for: s, ls;
   
   declarations 
      copyAndFill: 
      copyAndFill#(m, m0, n, a; ar, ar0){ar0 := copy(ar, m, ar0, m0, n); ar := fill(ar, a, m, m + n)};
      
      
      moveAndFill: 
      moveAndFill#(m, m0, n, a; ar)
      {ar := move(ar, m, m0, n); 
       if m ≤ n
       then if m + n < m0 then ar := fill(ar, a, m, n) else ar := fill(ar, a, m, m0)
       else if m + n < m + m - m0 then ar := fill(ar, a, m, n) else ar := fill(ar, a, m, m0)
      };
      
      
   
   
end enrich