Inverse in place

Inversing a permutation, in place

Topics: Array Data Structure / Permutation

Tools: Why3

References: The Art of Computer Programming

see also the index (by topic, by tool, by reference, by year)

```(*
Inverse of a permutation, in place
Algorithm I
The Art of Computer Programming, volume 1, Sec. 1.3.3, page 176

The idea is to inverse each orbit at a time, using negative values to
denote elements already inversed. The main loop scans the array and
proceeds as follows: a negative value -x-1 is simply changed into x; a
nonnegative value is the topmost element of a new orbit, which is
inversed by the inner loop.

Authors: Martin Clochard (École Normale Supérieure)
Jean-Christophe Filliâtre (CNRS)
*)

module InverseInPlace

use int.Int
use int.NumOf
use ref.Ref
use array.Array

let function (~_) (x: int) : int = -x-1

function numof (m: M.map int int) (l r: int) : int =
NumOf.numof (fun n -> M.([]) m n >= 0) l r

predicate is_permutation (a: array int) =
forall i: int. 0 <= i < length a ->
0 <= a[i] < length a /\
forall j: int. 0 <= j < length a -> i <> j -> a[i] <> a[j]

lemma is_permutation_inverse:
forall a b: array int. length a = length b ->
is_permutation a ->
(forall i: int. 0 <= i < length b -> 0 <= b[i] < length b) ->
(forall i: int. 0 <= i < length b -> a[b[i]] = i) ->
is_permutation b

predicate loopinvariant (olda a: array int) (m m' n: int) =
(forall e: int. 0 <= e < n -> -n <= a[e] < n)
/\ (forall e: int. m < e < n -> 0 <= a[e])
/\ (forall e: int. m < e < n -> olda[a[e]] = e)
/\ (forall e: int. 0 <= e <= m' -> a[e] >= 0 -> olda[e] = a[e])
/\ (forall e: int. 0 <= e <= m -> a[e] <= m)
/\ (forall e: int. 0 <= e <= m' -> a[e] < 0 ->
olda[~ a[e]] = e /\ (~a[e] <= m -> a[~a[e]] < 0))

let inverse_in_place (a: array int)
requires { is_permutation a }
ensures  { is_permutation a }
ensures  { forall i: int. 0 <= i < length a -> (old a)[a[i]] = i }
= let n = length a in
for m = n-1 downto 0 do
invariant { loopinvariant (old a) a m m n }
let i = ref a[m] in
if !i >= 0 then begin
(* unrolled loop once *)
a[m] <- -1;
let j = ref (~m) in
let k = ref !i in
i := a[!i];
while !i >= 0 do
invariant { a[!k] = !i <= m /\ 0 <= !k <= m /\ ~m <= !j < 0 /\
(old a)[~ !j] = !k /\ a[~ !j] < 0 /\ a[m] < 0 }
invariant { forall e: int. 0 <= e < m -> a[e] < 0 -> a[e] <> !j }
invariant { loopinvariant (old a) a m (m-1) n }
variant   { numof a.elts 0 n }
a[!k] <- !j;
j := ~ !k;
k := !i;
i := a[!k]
done;
assert { !k = m };
i := !j
end;
assert { (old a)[~ !i] = m };
a[m] <- ~ !i
done

end

module Harness

use array.Array
use InverseInPlace

(* (0 2) (1) *)
let test1 () =
let a = make 3 0 in
a[0] <- 2; a[2] <- 0; a[1] <- 1;
inverse_in_place a;
a

(* (0 1 2) *)
let test2 () =
let a = make 3 0 in
a[0] <- 1; a[1] <- 2; a[2] <- 0;
inverse_in_place a;
a

end

(*
Local Variables:
compile-command: "why3ide inverse_in_place.mlw"
End:
*)
```