Maj terminée. Pour consulter la release notes associée voici le lien :
 Jean-Christophe Filliâtre committed Aug 05, 2011 1 2 3 4 5 6 7 8 `````` (* 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 `````` Guillaume Melquiond committed Mar 24, 2016 9 10 `````` use int.Iter `````` Jean-Christophe Filliâtre committed Aug 05, 2011 11 `````` `````` Jean-Christophe Filliâtre committed Aug 05, 2011 12 `````` type t `````` Guillaume Melquiond committed Mar 24, 2016 13 14 15 16 17 `````` val predicate eq (x y : t) ensures { result <-> x = y } (* let f be a function from t to t *) val function f t : t `````` Jean-Christophe Filliâtre committed Aug 05, 2011 18 `````` `````` Jean-Christophe Filliâtre committed Aug 05, 2011 19 `````` (* given some initial value x0 *) `````` Guillaume Melquiond committed Mar 24, 2016 20 `````` val constant x0: t `````` Jean-Christophe Filliâtre committed Aug 05, 2011 21 `````` `````` Jean-Christophe Filliâtre committed Aug 05, 2011 22 `````` (* we can build the infinite sequence defined by x{i+1} = f(xi) *) `````` Guillaume Melquiond committed Mar 24, 2016 23 `````` function x (i: int): t = Iter.iter f i x0 `````` Jean-Christophe Filliâtre committed Aug 05, 2011 24 25 26 27 28 29 30 31 `````` (* let use assume now that the sequence (x_i) has finitely many distinct values (e.g. f is an integer function with values in 0..m) it means that there exists values lambda and mu such that (1) x0, x1, ... x{mu+lambda-1} are all distinct, and (2) x{n+lambda} = x_n when n >= mu. *) `````` Jean-Christophe Filliâtre committed Aug 05, 2011 32 33 `````` (* lambda and mu are skomlemized *) `````` Jean-Christophe Filliâtre committed Feb 06, 2012 34 35 `````` constant mu : int constant lambda : int `````` Jean-Christophe Filliâtre committed Aug 05, 2011 36 `````` `````` Jean-Christophe Filliâtre committed Aug 05, 2011 37 `````` (* they are axiomatized as follows *) `````` Jean-Christophe Filliâtre committed Aug 05, 2011 38 `````` axiom mu_range: 0 <= mu `````` Jean-Christophe Filliâtre committed Aug 05, 2011 39 `````` `````` Jean-Christophe Filliâtre committed Aug 05, 2011 40 41 42 43 44 45 46 47 `````` axiom lambda_range: 1 <= lambda axiom distinct: forall i j: int. 0 <= i < mu+lambda -> 0 <= j < mu+lambda -> i <> j -> x i <> x j axiom cycle: forall n: int. mu <= n -> x (n + lambda) = x n `````` Jean-Christophe Filliâtre committed Aug 05, 2011 48 49 50 `````` lemma cycle_induction: forall n: int. mu <= n -> forall k: int. 0 <= k -> x (n + lambda * k) = x n `````` Jean-Christophe Filliâtre committed Aug 05, 2011 51 `````` (* Now comes the code. `````` Jean-Christophe Filliâtre committed Aug 05, 2011 52 53 `````` Two references, tortoise and hare, traverses the sequence (xi) at speed 1 and 2 respectively. We stop whenever they are equal. `````` Jean-Christophe Filliâtre committed Aug 05, 2011 54 55 56 57 `````` The challenge is to prove termination. Actually, we even prove that the code runs in time O(lambda + mu). *) `````` Andrei Paskevich committed Oct 13, 2012 58 `````` use import ref.Ref `````` Jean-Christophe Filliâtre committed Aug 05, 2011 59 `````` `````` Jean-Christophe Filliâtre committed Aug 16, 2011 60 61 62 63 64 65 66 67 68 `````` (* the minimal distance between x i and x j *) function dist int int : int (* it is defined as soon as i,j >= mu *) axiom dist_def: forall i j: int. mu <= i -> mu <= j -> dist i j >= 0 /\ x (i + dist i j) = x j /\ forall k: int. 0 <= k -> x (i + k) = x j -> dist i j <= k `````` Jean-Christophe Filliâtre committed Aug 05, 2011 69 `````` predicate rel (t2 t1: t) = `````` Jean-Christophe Filliâtre committed Aug 16, 2011 70 71 `````` exists i: int. t1 = x i /\ t2 = x (i+1) /\ 1 <= i <= mu + lambda /\ (i >= mu -> dist (2*i+2) (i+1) < dist (2*i) i) `````` Jean-Christophe Filliâtre committed Aug 05, 2011 72 73 74 75 `````` let tortoise_hare () = let tortoise = ref (f x0) in let hare = ref (f (f x0)) in `````` Guillaume Melquiond committed Mar 24, 2016 76 `````` while not (eq !tortoise !hare) do `````` Jean-Christophe Filliâtre committed Aug 05, 2011 77 78 `````` invariant { exists t: int. `````` Jean-Christophe Filliâtre committed Aug 05, 2011 79 `````` 1 <= t <= mu+lambda /\ !tortoise = x t /\ !hare = x (2 * t) /\ `````` Jean-Christophe Filliâtre committed Aug 05, 2011 80 `````` forall i: int. 1 <= i < t -> x i <> x (2*i) } `````` Andrei Paskevich committed Oct 13, 2012 81 `````` variant { !tortoise with rel } `````` Jean-Christophe Filliâtre committed Aug 05, 2011 82 83 84 85 86 87 88 `````` tortoise := f !tortoise; hare := f (f !hare) done (* TODO: code to find out lambda and mu. See wikipedia. *) end``````