int e := ?; @pre true @post ((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 j := 0; for @ true (int i := 0; i < |a|; i := i + 1) { u[j] := a[i]; j := j + 1; } for @ true (int i := 0; i < |b|; i := i + 1) { u[j] := b[i]; j := j + 1; } return u; }