#include "arrays.pi"

define int e = ?;

@pre  true
@post ((exists(ix, 0, length(a) - 1, a[ix] == e)
           || exists(ix, 0, length(b) - 1, b[ix] == e))
          -> exists(ix, 0, length(rv) - 1, rv[ix] == e))
      && (exists(ix, 0, length(rv) - 1, rv[ix] == e)
          -> (exists(ix, 0, length(a) - 1, a[ix] == e)
              || exists(ix, 0, length(b) - 1, b[ix] == e)))
int[] union(int[] a, int[] b)
declare
  int i, j;
  int[] u;
{
  u = new int[length(a) + length(b)];
  j = 0;

  for
    @ true
    (i = 0; i < length(a); i = i + 1)
  {
    u[j] = a[i];
    j = j + 1;
  }
  for
    @ true
    (i = 0; i < length(b); i = i + 1)
  {
    u[j] = b[i];
    j = j + 1;
  }

  return u;
}