proof of algo64

.gitignore

@@ -177,7 +177,6 @@ pvsbin/
 /examples/programs/vacid_0_red_black_trees_harness/
 /examples/programs/next_digit_sum/
 /examples/programs/algo63/
-/examples/programs/algo64/
 /examples/programs/algo65/
 /examples/programs/binary_search_c/
 /examples/programs/dijkstra/

examples/programs/algo64.mlw

@@ -18,12 +18,7 @@ module Algo64
   use import module ref.Ref
   use import module array.Array
   use import module array.ArrayPermut
-
-  predicate sorted_sub (a: array int) (l u: int)
-(*
-  clone import module array.ArraySorted with
-    type elt = int, predicate le = (<=)
-*)
+  use import module array.ArraySorted
 
   (* Algorithm 63 *)
 
@@ -31,7 +26,7 @@ module Algo64
     a:array int -> m:int -> n:int -> i:ref int -> j:ref int ->
     { 0 <= m < n < length a }
     unit writes a i j
-    { m <= !j < !i <= n /\ permut_sub (old a) a m n /\
+    { m <= !j < !i <= n /\ permut_sub (old a) a m (n+1) /\
       exists x:int.
         (forall r:int. m <= r <= !j -> a[r] <= x) /\
         (forall r:int. !j < r < !i -> a[r] = x) /\
@@ -47,11 +42,11 @@ module Algo64
       let j = ref 0 in
       partition a m n i j;
 'L1:  quicksort a m !j;
-      assert { permut_sub (at a 'L1) a m n };
+      assert { permut_sub (at a 'L1) a m (n+1) };
 'L2:  quicksort a !i n;
-      assert { permut_sub (at a 'L2) a m n }
+      assert { permut_sub (at a 'L2) a m (n+1) }
     end
-    { permut_sub (old a) a m n /\ sorted_sub a m n }
+    { permut_sub (old a) a m (n+1) /\ sorted_sub a m (n+1) }
 
 end