algo64.mlw 1.65 KB
Newer Older
1
(***
2

3 4
Algorithm 64

5
C. A. R. Hoare
6 7 8 9
Elliott Brothers Ltd., Hertfordshire, England, U.K.

Communications of the ACM  archive
Volume 4 ,  Issue 7  (July 1961) table of contents
10
Pages: 321 - 322
11 12 13 14 15

***)

module Algo64

16 17 18 19 20
  use int.Int
  use ref.Ref
  use array.Array
  use array.ArrayPermut
  use array.IntArraySorted
21

22 23
  (* Algorithm 63 *)

24 25
  val partition (a: array int) (m n: int) (i j: ref int) (ghost x: ref int) :
    unit
26
    requires { 0 <= m < n < length a }
27
    writes   { a, i, j }
28 29
    ensures  { m <= !j < !i <= n }
    ensures  { permut_sub (old a) a m (n+1) }
30 31 32
    ensures  { forall r:int. m <= r <= !j -> a[r] <= !x }
    ensures  { forall r:int. !j < r < !i -> a[r] = !x }
    ensures  { forall r:int. !i <= r <= n -> a[r] >= !x }
33

34 35
  (* Algorithm 64 *)

36 37 38 39 40 41
  predicate qs_partition (t1 t2: array int) (m n i j: int) (x: int) =
    permut_sub t1 t2 m (n+1) /\
    (forall k:int. m <= k <= j  -> t2[k] <= x) /\
    (forall k:int. j <  k <  i  -> t2[k] =  x) /\
    (forall k:int. i <= k <= n ->  t2[k] >= x)

42
  let rec quicksort (a:array int) (m n:int) : unit
43
    requires { 0 <= m <= n < length a }
44
    variant  { n - m }
45 46
    ensures  { permut_sub (old a) a m (n+1) }
    ensures  { sorted_sub a m (n+1) }
47
  = if m < n then begin
48 49
      let i = ref 0 in
      let j = ref 0 in
50 51
      let ghost x = ref 42 in
      partition a m n i j x;
52 53 54 55 56 57
    label L1 in
      quicksort a m !j;
      assert { qs_partition (a at L1) a m n !i !j !x };
    label L2 in
      quicksort a !i n;
      assert { qs_partition (a at L2) a m n !i !j !x }
58 59
    end

60
  let qs (a:array int) : unit
61
    ensures  { permut_all (old a) a }
62 63 64
    ensures  { sorted a }
  = if length a > 0 then quicksort a 0 (length a - 1)

65
end