6 Elliott Brothers Ltd., Hertfordshire, England, U.K.
8 Communications of the ACM archive
9 Volume 4 , Issue 7 (July 1961) table of contents
23 val partition (a: array int) (m n: int) (i j: ref int) (ghost x: ref int) :
25 requires { 0 <= m < n < length a }
27 ensures { m <= !j < !i <= n }
28 ensures { permut_sub (old a) a m (n+1) }
29 ensures { forall r:int. m <= r <= !j -> a[r] <= !x }
30 ensures { forall r:int. !j < r < !i -> a[r] = !x }
31 ensures { forall r:int. !i <= r <= n -> a[r] >= !x }
33 (* Algorithm 65 (fixed version) *)
35 let rec find (a: array int) (m n: int) (k: int) : unit
36 requires { 0 <= m <= k <= n < length a }
38 ensures { permut_sub (old a) a m (n+1) }
39 ensures { forall r:int. m <= r <= k -> a[r] <= a[k] }
40 ensures { forall r:int. k <= r <= n -> a[k] <= a[r] }
44 let ghost x = ref 42 in
45 partition a m n i j x;
47 if k <= !j then find a m !j k;
48 assert { permut_sub (a at L1) a m (n+1) };
49 assert { forall r:int. !j < r <= n -> a[r] = (a at L1)[r] };
50 assert { forall r:int. m <= r <= !j ->
51 (exists s:int. m <= s <= !j /\ a[r] = (a at L1)[s]) &&
54 if !i <= k then find a !i n k;
55 assert { permut_sub (a at L2) a m (n+1) };
56 assert { forall r:int. m <= r < !i -> a[r] = (a at L2)[r] };
57 assert { forall r:int. !i <= r <= n ->
58 (exists s:int. !i <= s <= n /\ a[r] = (a at L2)[s]) &&