inverse_in_place completed (with the help of Martin)

examples/in_progress/inverse_in_place.mlw → examples/inverse_in_place.mlw

@@ -9,6 +9,10 @@
   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
@@ -39,39 +43,14 @@ module InverseInPlace
     (forall i: int. 0 <= i < length b -> a[b[i]] = i) ->
     is_permutation b
 
-(***
-  predicate is_permutation_neg (a: array int) =
-    forall i: int. 0 <= i < length a ->
-      - (length a) <= a[i] < length a /\
-      forall j: int. 0 <= j < length a -> i <> j ->
-                     a[i] <> a[j] /\ a[i] <> lnot a[j]
-
-  lemma is_permutation_neg_is_permutation:
-    forall a: array int. is_permutation_neg a ->
-    (forall i: int. 0 <= i < length a -> 0 <= a[i]) ->
-    is_permutation a
-***)
-
-(*
-  predicate nodup (a: M.map int int) (m: int) =
-    forall i j: int. 0 <= i < j < m ->
-       (M.get a i <> M.get a j /\ M.get a i <> ~ (M.get a j))
-    \/ (M.get a i = ~ (M.get a j) = m)
-    \/ (~ (M.get a i) = M.get a j = m)
-*)
-
-  inductive orbit (array int) int int int =
-  | orbitO:
-      forall a: array int, x: int. orbit a x x 0
-  | orbitS:
-      forall a: array int, x y s: int. orbit a x y s -> orbit a x a[y] (s+1)
-  (** [orbit a x y s] means y=a^s(x) *)
-
-  lemma orbit1: forall a: array int, x: int. orbit a x a[x] 1
-
-  lemma orbit_permutation_1:
-    forall a: array int. is_permutation a ->
-    forall x y s: int. 0 <= x < length a -> orbit a x y s -> 0 <= y < length a
+  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 }
@@ -80,38 +59,19 @@ module InverseInPlace
   =
  'L:let n = length a in
     for m = n-1 downto 0 do
-      invariant { forall e: int. 0 <= e < n -> -n <= a[e] < n }
-      invariant { forall e: int. m < e < n -> 0 <= a[e] }
-      invariant { forall e: int. m < e < n -> (at a 'L)[a[e]] = e }
-      invariant { forall e: int. 0 <= e <= m -> a[e] < 0 ->
-                  (at a 'L)[~ a[e]] = e }
-      invariant { forall e: int. 0 <= e <= m -> a[e] >= 0 ->
-                  (at a 'L)[e] = a[e] }
-      invariant { forall e: int. 0 <= e <= m -> a[e] >= 0 ->
-                  forall y s: int. orbit (at a 'L) a[e] y s -> 0 <= y <= m }
+      invariant { loopinvariant (at a 'L) a m m n }
       let i = ref a[m] in
       if !i >= 0 then begin
         (* unrolled loop once *)
-        assert { orbit (at a 'L) m !i 1 };
         a[m] <- -1;
         let j = ref (~m) in
         let k = ref !i in
         i := a[!i];
-        assert { orbit (at a 'L) m !k 1 };
-        assert { 0 <= !i -> orbit (at a 'L) m !i 2 };
-        (* TODO: a ghost reference to count number of steps *)
         while !i >= 0 do
-          invariant { a[!k] = !i <= m /\ 0 <= !k <= m /\ -n <= !j < 0 /\
-                      (at a 'L)[~ !j] = !k /\ a[m] < 0 }
-          invariant { forall e: int. 0 <= e < n -> -n <= a[e] < n }
-          invariant { forall e: int. m < e < n -> 0 <= a[e] }
-          invariant { forall e: int. m < e < n -> (at a 'L)[a[e]] = e }
-          invariant { forall e: int. 0 <= e < m ->
-                      a[e] < 0 -> (at a 'L)[~ a[e]] = e }
-          invariant { forall e: int. 0 <= e < m ->
-                      a[e] >= 0 -> (at a 'L)[e] = a[e] }
-          invariant { forall e: int. 0 <= e < m -> a[e] >= 0 ->
-                      forall y s: int. orbit (at a 'L) a[e] y s -> 0 <= y <= m }
+          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   { num_of a.elts 0 n }
           a[!k] <- !j;
           j := ~ !k;