examples/inverse_in_place.mlw

   1
   2 (*
   3   Inverse of a permutation, in place
   4     Algorithm I
   5     The Art of Computer Programming, volume 1, Sec. 1.3.3, page 176
   6
   7   The idea is to inverse each orbit at a time, using negative values to
   8   denote elements already inversed. The main loop scans the array and
   9   proceeds as follows: a negative value -x-1 is simply changed into x; a
  10   nonnegative value is the topmost element of a new orbit, which is
  11   inversed by the inner loop.
  12
  13   Authors: Martin Clochard (École Normale Supérieure)
  14            Jean-Christophe Filliâtre (CNRS)
  15            Andrei Paskevich (Université Paris Sud)
  16 *)
  17
  18 module InverseInPlace
  19
  20   use int.Int
  21   use int.NumOf
  22   use ref.Ref
  23   use array.Array
  24
  25   let function (~_) (x: int) : int = -x-1
  26
  27   function numof (m: int -> int) (l r: int) : int =
  28     NumOf.numof (fun n -> m n >= 0) l r
  29
  30   predicate is_permutation (a: array int) =
  31     forall i. 0 <= i < length a ->
  32       0 <= a[i] < length a /\
  33       forall j. 0 <= j < length a -> i <> j -> a[i] <> a[j]
  34
  35   lemma is_permutation_inverse:
  36     forall a b: array int. length a = length b ->
  37     is_permutation a ->
  38     (forall i. 0 <= i < length b -> 0 <= b[i] < length b) ->
  39     (forall i. 0 <= i < length b -> a[b[i]] = i) ->
  40     is_permutation b
  41
  42   predicate loopinvariant (olda a: array int) (m m' n: int) =
  43       (forall e. 0 <= e < n -> -n <= a[e] < n)
  44    /\ (forall e. m < e < n -> 0 <= a[e])
  45    /\ (forall e. m < e < n -> olda[a[e]] = e)
  46    /\ (forall e. 0 <= e <= m' -> a[e] >= 0 -> olda[e] = a[e])
  47    /\ (forall e. 0 <= e <= m -> a[e] <= m)
  48    /\ (forall e. 0 <= e <= m' -> a[e] < 0 ->
  49         olda[~ a[e]] = e /\ (~a[e] <= m -> a[~a[e]] < 0))
  50
  51   let inverse_in_place (a: array int)
  52     requires { is_permutation a }
  53     ensures  { is_permutation a }
  54     ensures  { forall i. 0 <= i < length a -> (old a)[a[i]] = i }
  55   = let n = length a in
  56     for m = n - 1 downto 0 do
  57       invariant { loopinvariant (old a) a m m n }
  58       let ref i = a[m] in
  59       if i >= 0 then begin
  60         (* unrolled loop once *)
  61         a[m] <- -1;
  62         let ref j = (~m) in
  63         let ref k = i in
  64         i := a[i];
  65         while i >= 0 do
  66           invariant { a[k] = i <= m /\ 0 <= k <= m /\ ~m <= j < 0 /\
  67                       (old a)[~ j] = k /\ a[~ j] < 0 /\ a[m] < 0 }
  68           invariant { forall e. 0 <= e < m -> a[e] < 0 -> a[e] <> j }
  69           invariant { loopinvariant (old a) a m (m-1) n }
  70           variant   { numof a.elts 0 n }
  71           a[k] <- j;
  72           j := ~ k;
  73           k := i;
  74           i := a[k]
  75         done;
  76         assert { k = m };
  77         i := j
  78       end;
  79       assert { (old a)[~ i] = m };
  80       a[m] <- ~ i
  81     done
  82
  83 end
  84
  85 module Harness
  86
  87   use array.Array
  88   use InverseInPlace
  89
  90   (* (0 2) (1) *)
  91   let test1 () =
  92     let a = make 3 0 in
  93     a[0] <- 2; a[2] <- 0; a[1] <- 1;
  94     inverse_in_place a;
  95     a
  96
  97   (* (0 1 2) *)
  98   let test2 () =
  99     let a = make 3 0 in
 100     a[0] <- 1; a[1] <- 2; a[2] <- 0;
 101     inverse_in_place a;
 102     a
 103
 104 end
 105
 106 (*
 107 Local Variables:
 108 compile-command: "why3 ide inverse_in_place.mlw"
 109 End:
 110 *)