cleaning up examples for the gallery

parent 5e465f13
(* Binary search
A classical example. Searches a sorted array for a given value v. *)
module M
use import int.Int
......@@ -5,11 +9,6 @@ module M
use import module stdlib.Ref
use import module stdlib.Array
(* Binary search
The classical example. Searches a sorted array for a given value v.
*)
(* the code and its specification *)
exception Break int (* raised to exit the loop *)
......
module M
(* Bresenham line drawing algorithm. *)
use import int.Int
use import module stdlib.Ref
(* Parameters.
Without loss of generality, we can take [x1=0] and [y1=0].
Thus the line to draw joins [(0,0)] to [(x2,y2)]
and we have [deltax = x2] and [deltay = y2].
Moreover we assume being in the first octant, i.e.
[0 <= y2 <= x2]. The seven other cases can be easily
deduced by symmetry. *)
logic x2 : int
logic y2 : int
axiom First_octant : 0 <= y2 <= x2
(* The code.
[(best x y)] expresses that the point [(x,y)] is the best
possible point i.e. the closest to the real line (see the Coq file).
The invariant relates [x], [y] and [e] and
gives lower and upper bound for [e] (see the Coq file). *)
use import int.Abs
logic best (x y:int) =
forall y':int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2)
logic invariant_ (x y e:int) =
e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and
2 * (y2 - x2) <= e <= 2 * y2
lemma Invariant_is_ok : forall x y e:int. invariant_ x y e -> best x y
module M
let bresenham () =
let x = ref 0 in
let y = ref 0 in
let e = ref (2 * y2 - x2) in
while !x <= x2 do
invariant {0 <= x and x <= x2 + 1 and invariant_ x y e }
variant { x2 + 1 - x }
(* here we would plot (x, y) *)
assert { best x y };
if !e < 0 then
e := !e + 2 * y2
else begin
y := !y + 1;
e := !e + 2 * (y2 - x2)
end;
x := !x + 1
done
use import int.Int
use import module stdlib.Ref
(* Parameters.
Without loss of generality, we can take [x1=0] and [y1=0].
Thus the line to draw joins [(0,0)] to [(x2,y2)]
and we have [deltax = x2] and [deltay = y2].
Moreover we assume being in the first octant, i.e.
[0 <= y2 <= x2]. The seven other cases can be easily
deduced by symmetry. *)
logic x2 : int
logic y2 : int
axiom First_octant : 0 <= y2 <= x2
(* The code.
[(best x y)] expresses that the point [(x,y)] is the best
possible point i.e. the closest to the real line (see the Coq file).
The invariant relates [x], [y] and [e] and
gives lower and upper bound for [e] (see the Coq file). *)
use import int.Abs
logic best (x y:int) =
forall y':int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2)
logic invariant_ (x y e:int) =
e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and
2 * (y2 - x2) <= e <= 2 * y2
lemma Invariant_is_ok : forall x y e:int. invariant_ x y e -> best x y
let bresenham () =
let x = ref 0 in
let y = ref 0 in
let e = ref (2 * y2 - x2) in
while !x <= x2 do
invariant {0 <= x and x <= x2 + 1 and invariant_ x y e }
variant { x2 + 1 - x }
(* here we would plot (x, y) *)
assert { best x y };
if !e < 0 then
e := !e + 2 * y2
else begin
y := !y + 1;
e := !e + 2 * (y2 - x2)
end;
x := !x + 1
done
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/bresenham"
compile-command: "unset LANG; make -C ../.. examples/programs/bresenham.gui"
End:
*)
(* Sorting a list of integers using insertion sort *)
module M
use import int.Int
......@@ -5,24 +8,24 @@ module M
use import list.Sorted
use import list.Permut
let rec insert x l variant { length l } =
{ sorted l }
match l with
| Nil -> Cons x Nil
| Cons y r -> if x <= y then Cons x l else Cons y (insert x r)
end
{ sorted result and permut (Cons x l) result }
let rec insertion_sort l variant { length l } =
{ }
match l with
| Nil -> Nil
| Cons x r -> insert x (insertion_sort r)
end
{ sorted result and permut l result }
let rec insert x l variant { length l } =
{ sorted l }
match l with
| Nil -> Cons x Nil
| Cons y r -> if x <= y then Cons x l else Cons y (insert x r)
end
{ sorted result and permut (Cons x l) result }
let rec insertion_sort l variant { length l } =
{ }
match l with
| Nil -> Nil
| Cons x r -> insert x (insertion_sort r)
end
{ sorted result and permut l result }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/insertion_sort_list.gui"
......
(* Integer square root *)
module M
use import int.Int
......@@ -20,16 +23,13 @@ module M
let main () =
{ }
let r = isqrt 17 in
(* assert { r < 4 -> false };
assert { r > 4 -> false }; *)
r
isqrt 17
{ result = 4 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/isqrt"
compile-command: "unset LANG; make -C ../.. examples/programs/isqrt.gui"
End:
*)
(* McCarthy's ``91'' function. *)
module M
use import int.Int
(**** McCarthy's ``91'' function. *)
(* traditional recursive implementation *)
let rec f91 (n:int) : int variant { 101-n } =
{ }
if n <= 100 then
f91 (f91 (n + 11))
else
n - 10
{ (n <= 100 and result = 91) or (n >= 101 and result = n - 10) }
let rec f91 (n:int) : int variant { 101-n } =
{ }
if n <= 100 then
f91 (f91 (n + 11))
else
n - 10
{ (n <= 100 and result = 91) or (n >= 101 and result = n - 10) }
(* non-recursive version *)
(* non-recursive implementation using a while loop *)
use import module stdlib.Ref
......@@ -31,22 +33,22 @@ let rec f91 (n:int) : int variant { 101-n } =
clone import relations.Lex with type t1 = int, type t2 = int,
logic rel1 = lt_nat, logic rel2 = lt_nat
let f91_nonrec (n x : ref int) =
{ n >= 1 }
label L:
while !n > 0 do
invariant { n >= 0 and iter_f n x = iter_f (at n L) (at x L) }
variant { (101 - x + 10 * n, n) } with lex
if !x > 100 then begin
x := !x - 10;
n := !n - 1
end else begin
x := !x + 11;
n := !n + 1
end
done;
!x
{ result = iter_f (old n) (old x) }
let f91_nonrec (n x : ref int) =
{ n >= 1 }
label L:
while !n > 0 do
invariant { n >= 0 and iter_f n x = iter_f (at n L) (at x L) }
variant { (101 - x + 10 * n, n) } with lex
if !x > 100 then begin
x := !x - 10;
n := !n - 1
end else begin
x := !x + 11;
n := !n + 1
end
done;
!x
{ result = iter_f (old n) (old x) }
end
......
(* Sorting a list of integers using mergesort *)
module M
use import int.Int
......@@ -6,47 +9,47 @@ module M
use import list.Append
use import list.Permut
lemma Permut_append:
lemma Permut_append:
forall l1 l2 k1 k2 : list 'a.
permut l1 k1 -> permut l2 k2 -> permut (l1 ++ l2) (k1 ++ k2)
lemma Permut_cons_append:
forall x : 'a, l1 l2 : list 'a.
permut (Cons x l1 ++ l2) (l1 ++ Cons x l2)
lemma Permut_cons_append:
forall x : 'a, l1 l2 : list 'a.
permut (Cons x l1 ++ l2) (l1 ++ Cons x l2)
let split l0 =
{ length l0 >= 2 }
let rec split_aux (l1 : list 'a) l2 l variant { length l } =
{ length l2 = length l1 or length l2 = length l1 + 1 }
match l with
| Nil -> (l1, l2)
| Cons x r -> split_aux l2 (Cons x l1) r
end
{ let r1, r2 = result in
(length r2 = length r1 or length r2 = length r1 + 1) and
permut (r1 ++ r2) (l1 ++ (l2 ++ l)) }
in
split_aux Nil Nil l0
{ let (l1, l2) = result in
1 <= length l1 and 1 <= length l2 and permut l0 (l1 ++ l2) }
let rec merge l1 l2 variant { length l1 + length l2 } =
{ sorted l1 and sorted l2 }
match l1, l2 with
| Nil, _ -> l2
| _, Nil -> l1
| Cons x1 r1, Cons x2 r2 ->
if x1 <= x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2)
end
{ sorted result and permut result (l1 ++ l2) }
let split l0 =
{ length l0 >= 2 }
let rec split_aux (l1 : list 'a) l2 l variant { length l } =
{ length l2 = length l1 or length l2 = length l1 + 1 }
let rec mergesort l variant { length l } =
{ }
match l with
| Nil -> (l1, l2)
| Cons x r -> split_aux l2 (Cons x l1) r
| Nil | Cons _ Nil -> l
| _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2)
end
{ let r1, r2 = result in
(length r2 = length r1 or length r2 = length r1 + 1) and
permut (r1 ++ r2) (l1 ++ (l2 ++ l)) }
in
split_aux Nil Nil l0
{ let (l1, l2) = result in
1 <= length l1 and 1 <= length l2 and permut l0 (l1 ++ l2) }
let rec merge l1 l2 variant { length l1 + length l2 } =
{ sorted l1 and sorted l2 }
match l1, l2 with
| Nil, _ -> l2
| _, Nil -> l1
| Cons x1 r1, Cons x2 r2 ->
if x1 <= x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2)
end
{ sorted result and permut result (l1 ++ l2) }
let rec mergesort l variant { length l } =
{ }
match l with
| Nil | Cons _ Nil -> l
| _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2)
end
{ sorted result and permut l result }
{ sorted result and permut l result }
end
......
......@@ -17,7 +17,6 @@ theory Power
lemma Power_mult : forall x n m : int. 0 <= n -> 0 <= m ->
power x (n * m) = power (power x n) m
end
module M
......@@ -26,6 +25,8 @@ module M
use import int.ComputerDivision
use import Power
(* recursive implementation *)
let rec fast_exp x n variant { n } =
{ 0 <= n }
if n = 0 then
......@@ -36,6 +37,8 @@ module M
end
{ result = power x n }
(* non-recursive implementation using a while loop *)
use import module stdlib.Ref
let fast_exp_imperative x n =
......
(* Sorting an array using quicksort, with partitioning a la Bentley.
We simply scan the segment l..r from left ro right, maintaining values
smaller than t[l] on the left part of it (in l+1..m).
Then we swap t[l] and t[m] and we are done. *)
module Quicksort
use import int.Int
......
......@@ -46,7 +46,7 @@
"as"; "assert"; "begin";
"do"; "done"; "downto"; "else";
"exception"; "for"; "fun";
"exception"; "parameter"; "for"; "fun";
"if"; "in";
"module"; "mutable";
"rec"; "then"; "to";
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment