new programs: Hoare's algorithms 63-64-65

(Communications of the ACM)

examples/programs/algo63.mlw

+
+(***
+
+Algorithm 63
+   	
+C. A. R. Hoare 	 
+Elliott Brothers Ltd., Hertfordshire, England, U.K.
+
+Communications of the ACM  archive
+Volume 4 ,  Issue 7  (July 1961) table of contents
+Pages: 321 - 322   
+
+***)
+
+module Algo63
+
+  use import int.Int
+  use import module stdlib.Ref
+  use import module stdlib.Array
+  use import array.ArrayPermut
+
+  parameter partition : 
+    a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
+    { m < n } 
+    unit writes a i j
+    { m <= j and j < i and i <= n and permut (old a) a m n and
+      exists x:int.
+        (forall r:int. m <= r <= j -> a[r] <= x) and
+        (forall r:int. j < r < i -> a[r] = x) and
+        (forall r:int. i <= r <= n -> a[r] >= x) }
+
+end
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../.. examples/programs/algo63.gui"
+End: 
+*)

examples/programs/algo64.mlw

+
+(***
+   	
+Algorithm 64
+
+C. A. R. Hoare 	 
+Elliott Brothers Ltd., Hertfordshire, England, U.K.
+
+Communications of the ACM  archive
+Volume 4 ,  Issue 7  (July 1961) table of contents
+Pages: 321 - 322   
+
+***)
+
+module Algo64
+
+  use import int.Int
+  use import module stdlib.Ref
+  use import module stdlib.Array
+  use import array.ArrayPermut
+  clone import array.ArraySorted with type elt = int, logic le = (<=)
+ 
+  (* Algorithm 63 *)
+
+  parameter partition : 
+    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 and permut (old a) a m n and
+      exists x:int.
+        (forall r:int. m <= r <= j -> a[r] <= x) and
+        (forall r:int. j < r < i -> a[r] = x) and
+        (forall r:int. i <= r <= n -> a[r] >= x) }
+ 
+  (* Algorithm 64 *)
+
+  let rec quicksort (a:array int) (m:int) (n:int) : unit variant { n-m } =
+    { 0 <= m <= n < length a }
+    label Init:
+    if m < n then begin
+      let i = ref 0 in
+      let j = ref 0 in
+      partition a m n i j;
+      label L1:
+      quicksort a m !j;
+      assert { permut (at a L1) a m n };
+      label L2:
+      quicksort a !i n;
+      assert { permut (at a L2) a m n }
+    end
+    { permut (old a) a m n and sorted_sub a m n }
+
+end
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../.. examples/programs/algo64.gui"
+End: 
+*)
+
+

examples/programs/algo65.mlw

+
+(***
+   	
+Algorithm 65
+
+C. A. R. Hoare 	 
+Elliott Brothers Ltd., Hertfordshire, England, U.K.
+
+Communications of the ACM  archive
+Volume 4 ,  Issue 7  (July 1961) table of contents
+Pages: 321 - 322   
+
+***)
+
+module Algo65
+
+  use import int.Int
+  use import module stdlib.Ref
+  use import module stdlib.Array
+  use import array.ArrayPermut
+ 
+  (* algorithm 63 *)
+ 
+  parameter partition : 
+    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 and permut (old a) a m n and
+      exists x:int.
+        (forall r:int. m <= r <= j -> a[r] <= x) and
+        (forall r:int. j < r < i -> a[r] = x) and
+        (forall r:int. i <= r <= n -> a[r] >= x) }
+
+  (* Algorithm 65 (fixed version) *)
+
+  let rec find (a:array int) (m:int) (n:int) (k:int) : unit variant { n-m } =
+    { 0 <= m <= k <= n < length a }
+    if m < n then begin
+      let i = ref 0 in
+      let j = ref 0 in
+      label L1:
+      partition a m n i j;
+      assert { permut (at a L1) a m n };
+      label L2:
+      if k <= !j then find a m !j k;
+      assert { permut (at a L2) a m n };
+      if !i <= k then find a !i n k
+    end
+    { permut (old a) a m n and 
+      (forall r:int. m <= r <= k -> a[r] <= a[k]) and
+      (forall r:int. k <= r <= n -> a[k] <= a[r]) }
+
+end
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../.. examples/programs/algo65.gui"
+End: 
+*)