Quelle  concat_arrays.pvs

concat_arrays [n:nat, m:nat, T: TYPE]: THEORY
%------------------------------------------------------------------------
%
% This theory defines the concatenation operator o for arrays
%
%------------------------------------------------------------------------

BEGIN

  IMPORTING below_arrays

  a_n: VAR below_array[n,T]
  a_m: VAR below_array[m,T]
  nm : VAR below(n+m)

  o(a_n, a_m): below_array[n+m,T] = (LAMBDA nm: IF nm < n THEN a_n(nm)
                                                 ELSE a_m(nm - n)
                                                 ENDIF)

  i: VAR below(n)
  j: VAR {i: int | i >= n AND i < n+m}

  concat_array_bot0: THEOREM m = 0 IMPLIES a_n o a_m = a_n 

  concat_array_top0: THEOREM n = 0 IMPLIES a_n o a_m = a_m

  concat_array_bot : THEOREM (a_n o a_m)(i) = a_n(i)

  concat_array_top : THEOREM (a_n o a_m)(j) = a_m(j-n)

END concat_arrays