diff --git a/examples/programs/tortoise_and_hare.mlw b/examples/programs/tortoise_and_hare.mlw new file mode 100644 index 0000000000000000000000000000000000000000..1478306d035834ca3891bd3c85215d34d4f36704 --- /dev/null +++ b/examples/programs/tortoise_and_hare.mlw @@ -0,0 +1,71 @@ + +(* Floyd's cycle detection, also known as ``tortoise and hare'' algorithm. + + See The Art of Computer Programming, vol 2, exercise 6 page 7. *) + +module TortoiseAndHare + + use import int.Int + + (* let f be a function from 0..m-1 to 0..m-1 *) + function f int : int + function m : int + axiom dom_f: forall x: int. 0 <= x < m -> 0 <= f x < m + + (* let x0 be in 0..m-1 *) + function x0: int + axiom x0_range: 0 <= x0 < m + + (* let x_{i+1} = f(x_i) *) + clone import int.Iter with type t = int, function f = f + function x (i: int): int = iter i x0 + + (* lambda and mu are skomlemized *) + function mu : int + function lambda : int + + (* they are defined as follows *) + axiom mu_range: 0 <= mu + axiom lambda_range: 1 <= lambda + + (* values x0 ... x_{mu+lambda-1} are all distinct *) + axiom distinct: + forall i j: int. 0 <= i < mu+lambda -> 0 <= j < mu+lambda -> + i <> j -> x i <> x j + + (* cycle is lambda-long *) + axiom cycle: forall n: int. mu <= n -> x (n + lambda) = x n + + (* Now comes the code. + Two references, tortoise and hare, traverses the xi at speed 1 and 2. + + The challenge is to prove termination. + Actually, we even prove that the code runs in time O(lambda + mu). *) + + use import module ref.Ref + + predicate rel (t2 t1: int) = + exists i: int. t1 = x i /\ t2 = x (i+1) /\ 1 <= i <= lambda + mu + + let tortoise_hare () = + let tortoise = ref (f x0) in + let hare = ref (f (f x0)) in + while !tortoise <> !hare do + invariant { + exists t: int. + 1 <= t <= lambda+mu /\ !tortoise = x t /\ !hare = x (2 * t) /\ + forall i: int. 1 <= i < t -> x i <> x (2*i) } + variant { !tortoise } with rel + tortoise := f !tortoise; + hare := f (f !hare) + done + + (* TODO: code to find out lambda and mu. See wikipedia. *) + +end + +(* +Local Variables: +compile-command: "unset LANG; make -C ../.. examples/programs/tortoise_and_hare.gui" +End: +*) diff --git a/examples/programs/tortoise_and_hare/tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_2.v b/examples/programs/tortoise_and_hare/tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_2.v new file mode 100644 index 0000000000000000000000000000000000000000..1d871534cd06474f441dde4dae3d012473bffacb --- /dev/null +++ b/examples/programs/tortoise_and_hare/tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_2.v @@ -0,0 +1,135 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import ZArith. +Require Import Rbase. +Definition unit := unit. + +Parameter mark : Type. + +Parameter at1: forall (a:Type), a -> mark -> a. + +Implicit Arguments at1. + +Parameter old: forall (a:Type), a -> a. + +Implicit Arguments old. + +Parameter f: Z -> Z. + + +Parameter m: Z. + + +Axiom dom_f : forall (x:Z), ((0%Z <= x)%Z /\ (x < (m ))%Z) -> + ((0%Z <= (f x))%Z /\ ((f x) < (m ))%Z). + +Parameter x0: Z. + + +Axiom x0_range : (0%Z <= (x0 ))%Z /\ ((x0 ) < (m ))%Z. + +Parameter iter: Z -> Z -> Z. + + +Axiom iter_0 : forall (x:Z), ((iter 0%Z x) = x). + +Axiom iter_s : forall (k:Z) (x:Z), (0%Z < k)%Z -> ((iter k + x) = (iter (k - 1%Z)%Z (f x))). + +Axiom iter_1 : forall (x:Z), ((iter 1%Z x) = (f x)). + +Axiom iter_s2 : forall (k:Z) (x:Z), (0%Z < k)%Z -> ((iter k + x) = (f (iter (k - 1%Z)%Z x))). + +Parameter mu: Z. + + +Parameter lambda: Z. + + +Axiom mu_range : (0%Z <= (mu ))%Z. + +Axiom lambda_range : (1%Z <= (lambda ))%Z. + +Axiom distinct : forall (i:Z) (j:Z), ((0%Z <= i)%Z /\ + (i < ((mu ) + (lambda ))%Z)%Z) -> (((0%Z <= j)%Z /\ + (j < ((mu ) + (lambda ))%Z)%Z) -> ((~ (i = j)) -> ~ ((iter i + (x0 )) = (iter j (x0 ))))). + +Axiom cycle : forall (n:Z), ((mu ) <= n)%Z -> ((iter (n + (lambda ))%Z + (x0 )) = (iter n (x0 ))). + +Inductive ref (a:Type) := + | mk_ref : a -> ref a. +Implicit Arguments mk_ref. + +Definition contents (a:Type)(u:(ref a)): a := + match u with + | mk_ref contents1 => contents1 + end. +Implicit Arguments contents. + +Definition rel(t2:Z) (t1:Z): Prop := exists i:Z, (t1 = (iter i (x0 ))) /\ + ((t2 = (iter (i + 1%Z)%Z (x0 ))) /\ ((1%Z <= i)%Z /\ + (i <= ((lambda ) + (mu ))%Z)%Z)). + +Theorem WP_parameter_tortoise_hare : forall (hare:Z), forall (tortoise:Z), + (exists t:Z, ((1%Z <= t)%Z /\ (t <= ((lambda ) + (mu ))%Z)%Z) /\ + ((tortoise = (iter t (x0 ))) /\ ((hare = (iter (2%Z * t)%Z (x0 ))) /\ + forall (i:Z), ((1%Z <= i)%Z /\ (i < t)%Z) -> ~ ((iter i + (x0 )) = (iter (2%Z * i)%Z (x0 )))))) -> ((~ (tortoise = hare)) -> + forall (tortoise1:Z), (tortoise1 = (f tortoise)) -> forall (hare1:Z), + (hare1 = (f (f hare))) -> exists t:Z, ((1%Z <= t)%Z /\ + (t <= ((lambda ) + (mu ))%Z)%Z) /\ ((tortoise1 = (iter t (x0 ))) /\ + ((hare1 = (iter (2%Z * t)%Z (x0 ))) /\ forall (i:Z), ((1%Z <= i)%Z /\ + (i < t)%Z) -> ~ ((iter i (x0 )) = (iter (2%Z * i)%Z (x0 )))))). +(* YOU MAY EDIT THE PROOF BELOW *) +intros hare tortoise (t, (ht, (eqt, (eqh, h)))). +intros; subst. +assert (dis: forall i : Z, (1 <= i <= t)%Z -> iter i x0 <> iter (2 * i) x0). +intros i hi. +assert (case: (i < t \/ i = t)%Z) by omega. destruct case. +apply (h i); omega. +subst; omega. clear h H. + +exists (t + 1)%Z; intuition. +assert (case: (t+1 <= lambda + mu \/ t+1> lambda+mu)%Z) by omega. + destruct case. +assumption. +assert (t = lambda+mu)%Z by omega. subst. +clear H0 H1. +pose (i := (lambda+mu-(lambda+mu) mod lambda)%Z). +generalize lambda_range mu_range. intros hlam hmu. +assert (lambda_pos: (lambda > 0)%Z) by omega. +generalize (Z_mod_lt (lambda+mu) lambda lambda_pos)%Z. intro hr. +generalize (Z_div_mod_eq (lambda+mu) lambda lambda_pos)%Z. intro hq. +absurd (iter i x0 = iter (2*i) x0). +red; intro; apply (dis i); auto. +subst i; omega. +assert (hi: (mu <= i)%Z) by (subst i; omega). +assert (ind: (forall k: Z, 0 <= k -> iter (i + lambda*k) x0 = iter i x0)%Z). +apply natlike_ind. +ring_simplify (i + lambda * 0)%Z; auto. +intros. +unfold Zsucc. +replace (i + lambda * (x + 1))%Z with ((i+lambda*x)+lambda)%Z by ring. +rewrite cycle; auto. +assert (0 <= lambda * x)%Z. +apply Zmult_le_0_compat; omega. +omega. +replace (2*i)%Z with (i + lambda * ((lambda + mu) / lambda))%Z. +symmetry. apply ind. +apply Z_div_pos; omega. +subst i; omega. + +rewrite (iter_s2 (t+1)%Z); intuition. +ring_simplify (t+1-1)%Z; auto. +rewrite (iter_s2 (2*(t+1))%Z); intuition. +ring_simplify (2 * (t + 1) - 1) %Z. +rewrite (iter_s2 (2*t+1)%Z); intuition. +ring_simplify (2 * t + 1 - 1) %Z; auto. +apply (dis i); omega. +Qed. +(* DO NOT EDIT BELOW *) + + diff --git a/examples/programs/tortoise_and_hare/why3session.xml b/examples/programs/tortoise_and_hare/why3session.xml new file mode 100644 index 0000000000000000000000000000000000000000..11ba9aa0219e67485e863163a88bbf8650713d4d --- /dev/null +++ b/examples/programs/tortoise_and_hare/why3session.xml @@ -0,0 +1,32 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/programs/tortoise_hare.mlw b/examples/programs/tortoise_hare.mlw deleted file mode 100644 index 37e1857fd0b59bd65f7a4e7ce255d86fa49a34b6..0000000000000000000000000000000000000000 --- a/examples/programs/tortoise_hare.mlw +++ /dev/null @@ -1,73 +0,0 @@ - -(* Floyd's ``the tortoise and the hare'' algorithm. *) - -module TortoiseHare - - use import int.Int - - (* We consider a function f over an abstract type t *) - - type t - - function f t : t - - (* Given some x0 in t, we consider the sequence of the repeated calls - to f starting from x0. *) - - function x int : t - - axiom xdef: forall n:int. n >= 0 -> x (n+1) = f (x n) - - function x0 : t = x 0 - - (* If t is finite, this sequence will eventually end up on a cycle. - Let us simply assume the existence of this cycle, that is - x (i + lambda) = x i, for some lambda > 0 and i large enough. *) - - function mu : int - axiom mu: mu >= 0 - - function lambda : int - axiom lambda: lambda >= 1 - - axiom cycle: forall i:int. mu <= i -> x (i + lambda) = x i - - lemma cycle_gen: - forall i:int. mu <= i -> forall k:int. 0 <= k -> x (i + lambda * k) = x i - - (* The challenge is to prove that the recursive function - - let rec run x1 x2 = if x1 <> x2 then run (f x1) (f (f x2)) - - terminates when called on x0 and (f x0). - *) - - function dist int int : int - - axiom dist_def1: - forall n m: int. 0 <= n <= m -> - x (n + dist n m) = x m - axiom dist_def2: - forall n m: int. 0 <= n <= m -> - forall k: int. x (n + k) = x m -> dist n m <= k - - predicate r (x12 : (t, t)) (x'12 : (t, t)) = - let x1, x2 = x12 in - let x'1, x'2 = x'12 in - exists m:int. - x1 = x (m+1) /\ x2 = x (2*m+2) /\ x'1 = x m /\ x'2 = x (2*m) /\ - m < mu \/ (mu <= m /\ dist (m+1) (2*m+2) < dist m (2*m)) - - let rec run x1 x2 variant { (x1, x2) } with r = - { exists m:int [x m]. x1 = x m /\ x2 = x (2*m) } - if x1 <> x2 then - run (f x1) (f (f x2)) - { } - -end - -(* -Local Variables: -compile-command: "unset LANG; make -C ../.. examples/programs/tortoise_hare.gui" -End: -*)