## Inverse in place

Inversing a permutation, in place

Catégories: Array Data Structure / Permutation

Outils: Why3

Références: 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: int -> int) (l r: int) : int =
NumOf.numof (fun n -> m n >= 0) l r

predicate is_permutation (a: array int) =
forall i. 0 <= i < length a ->
0 <= a[i] < length a /\
forall j. 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. 0 <= i < length b -> 0 <= b[i] < length b) ->
(forall i. 0 <= i < length b -> a[b[i]] = i) ->
is_permutation b

predicate loopinvariant (olda a: array int) (m m' n: int) =
(forall e. 0 <= e < n -> -n <= a[e] < n)
/\ (forall e. m < e < n -> 0 <= a[e])
/\ (forall e. m < e < n -> olda[a[e]] = e)
/\ (forall e. 0 <= e <= m' -> a[e] >= 0 -> olda[e] = a[e])
/\ (forall e. 0 <= e <= m -> a[e] <= m)
/\ (forall e. 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. 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 ref i = a[m] in
if i >= 0 then begin
(* unrolled loop once *)
a[m] <- -1;
let ref j = (~m) in
let ref k = 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. 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: "why3 ide inverse_in_place.mlw"
End:
*)
```