| next#(; ar; hasNext) {let ghostar = ar in if # ar = 0 then hasNext := false else let i = (# ar)-1 in {while i > 0 ∧ ar[i -1] ≥ ar[i] do {/* next-perm: invariant i < # ar wfbound i; next-proper-permutation: invariant i < # ar ∧ ordered≤(rev(subarray(ar, i, # ar - i))) wfbound i */; i := i -1}; if i ≤ 0 then hasNext := false else {let j = (# ar)-1 in {while ar[j] ≤ ar[i -1] do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j; next-proper-permutation: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 ∧ ordered≤(rev(subarray(ar, i, # ar - i))) ∧ (∀ n. n > j ∧ n < # ar → ar[n] ≤ ar[i - 1]) wfbound j */; j := j -1}; let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; /* next-proper-permutation: ordered≤(rev(subarray(ar, i, # ar - i))) ∧ (∀ n. n ≥ j ∧ n < # ar → ar[n] < ar[i - 1]) ∧ ghostar ≠ ar ∧ ghostar ≤ ar ∧ ghostar[j] = ar[i - 1] */; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j; next-proper-permutation: invariant j < # ar ∧ i < # ar ∧ i ≠ 0 ∧ i` ≤ i ∧ perm(ghostar, ar) ∧ subarray(ghostar, 0, i` - 1) = subarray(ar, 0, i` - 1) ∧ ghostar[ghost_j] = ar[i` - 1] ∧ ( i < j → rev(subarray(ar`, i`, # ar - i`)) = subarray(ar, i`, i - i`) + rev(subarray(ar, i, j + 1 - i)) + subarray(ar, j + 1, # ar - j + 1)) ∧ (i ≥ j → rev(subarray(ar`, i`, # ar - i`)) = subarray(ar, i`, # ar - i`)) wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i +1; j := j -1}}}}; hasNext := true}} } |