algo64.mlw 1.37 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
16

***)

module Algo64

  use import int.Int
17
18
19
20
  use import ref.Ref
  use import array.Array
  use import array.ArrayPermut
  use import array.ArraySorted
21

22
23
  (* Algorithm 63 *)

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

35
36
37
  (* Algorithm 64 *)

  let rec quicksort (a:array int) (m:int) (n:int) : unit variant { n-m } =
38
39
40
    requires { 0 <= m <= n < length a }
    ensures  { permut_sub (old a) a m (n+1) }
    ensures  { sorted_sub a m (n+1) }
41
'Init:
42
43
44
45
    if m < n then begin
      let i = ref 0 in
      let j = ref 0 in
      partition a m n i j;
46
'L1:  quicksort a m !j;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
47
      assert { permut_sub (at a 'L1) a m (n+1) };
48
'L2:  quicksort a !i n;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
49
      assert { permut_sub (at a 'L2) a m (n+1) }
50
51
    end

52
53
54
55
56
  let qs (a:array int) : unit
    ensures  { permut (old a) a }
    ensures  { sorted a }
  = if length a > 0 then quicksort a 0 (length a - 1)

57
end