Given an array a that records an injective function 0..N-1 -> 0..M-1, compute the inverse b from 0..M-1 -> 0..N-1.
Prove that b[a[]i]] == i and a[b[j]] == j.
The challenge in this exercise is to identify the preconditions that clarify the problem.
public class InvertInjection {
static public int N;
static public int M;
static public int[] a;
static public int[] b;
//@ requires a != b; // Note - this is needed !
//@ requires 0 <= N <= a.length;
//@ requires 0 <= M <= b.length;
//@ requires \forall int i; 0 <= i < N; 0 <= a[i] < M;
//@ requires \forall int i,j; 0 <= i < j < N; a[i] != a[j];
//@ ensures \forall int i; 0 <= i < N; b[a[i]] == i;
//@ ensures \forall int i; 0 <= i < M; ((\forall int j; 0 <= j < N; a[j] != i) <==> b[i] == -1);
//@ ensures \forall int j; 0 <= j < M; b[j] != -1 ==> a[b[j]] == j;
public void invert() {
//@ loop_invariant 0 <= k <= M;
//@ loop_invariant \forall int i; 0 <= i < k; b[i] == -1;
//@ loop_decreases M - k;
for (int k = 0; k < M; k++) b[k] = -1;
//@ loop_invariant 0 <= k <= N;
//@ loop_invariant \forall int i; 0 <= i < k; b[a[i]] == i;
//@ loop_invariant \forall int i; 0 <= i < M; ((\forall int j; 0 <= j < k; a[j] != i) <==> b[i] == -1);
//@ loop_invariant \forall int j; 0 <= j < M; b[j] != -1 ==> a[b[j]] == j;
//@ loop_decreases N - k;
for (int k = 0; k < N; k++) {
b[a[k]] = k;
}
}
}