int e := ?;

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

	for
		@	true
		(int k := 0; k < |u|; k := k + 1)
	{
		if (i >= |a|) {
			u[k] := b[j];
			j := j + 1;
		}
		else if (j >= |b|) {
			u[k] := a[i];
			i := i + 1;
		}
		else if (a[i] <= b[j]) {
			u[k] := a[i];
			i := i + 1;
		}
		else {
			u[k] := b[j];
			j := j + 1;
		}
	}

	return u;
}