Toccata

(*
  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 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:
*)