Wiki Agenda Contact Version française

Inverse in place

Inversing a permutation, in place


Authors: Jean-Christophe Filliâtre / Andrei Paskevich / Martin Clochard

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)
           Andrei Paskevich (Université Paris Sud)
*)

module InverseInPlace

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

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

  function numof (m: M.map int int) (l r: int) : int =
    NumOf.numof (\ 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 (old 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 -> old[a[e]] = e)
   /\ (forall e: int. 0 <= e <= m' -> a[e] >= 0 -> old[e] = a[e])
   /\ (forall e: int. 0 <= e <= m -> a[e] <= m)
   /\ (forall e: int. 0 <= e <= m' -> a[e] < 0 ->
        old[~ 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 }
  =
 'L:let n = length a in
    for m = n-1 downto 0 do
      invariant { loopinvariant (at a 'L) 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 /\
                      (at a 'L)[~ !j] = !k /\ a[~ !j] < 0 /\ a[m] < 0 }
          invariant { forall e: int. 0 <= e < m -> a[e] < 0 -> a[e] <> !j }
          invariant { loopinvariant (at a 'L) 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 { (at a 'L)[~ !i] = m };
      a[m] <- ~ !i
    done

end

module Harness

  use import array.Array
  use import 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:
*)

download ZIP archive