algo63.mlw 804 Bytes
Newer Older
1 2 3 4

(***

Algorithm 63
5 6

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

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

***)

module Algo63

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

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

end

(*
35
Local Variables:
36
compile-command: "unset LANG; make -C ../.. examples/programs/algo63.gui"
37
End:
38
*)