From 8a6f9e754506d514e653d1dc1d02fde3d9bd8183 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Wed, 6 Jun 2018 12:47:53 +0200 Subject: [PATCH] tortoise and hare example totally revamped this is much closer now to TAOCP, vol 2, exercise 6 page 7 --- examples/tortoise_and_hare.mlw | 216 ++++++++---- examples/tortoise_and_hare/why3session.xml | 374 ++++++++++++++++++++- examples/tortoise_and_hare/why3shapes.gz | Bin 456 -> 3519 bytes 3 files changed, 502 insertions(+), 88 deletions(-) diff --git a/examples/tortoise_and_hare.mlw b/examples/tortoise_and_hare.mlw index cbfd1deb6..d80e2ab81 100644 --- a/examples/tortoise_and_hare.mlw +++ b/examples/tortoise_and_hare.mlw @@ -3,88 +3,162 @@ See The Art of Computer Programming, vol 2, exercise 6 page 7. *) -module TortoiseAndHare +module TortoiseAndHareAlgorithm use import int.Int - use int.Iter + use import int.EuclideanDivision + use import int.Iter + use import seq.Seq + use import seq.Distinct + use import ref.Refint + use import pigeon.Pigeonhole - type t - val predicate eq (x y : t) - ensures { result <-> x = y } + val function f int : int - (* let f be a function from t to t *) - val function f t : t + (* f maps 0..m-1 to 0..m-1 *) + constant m: int + axiom m_positive: m > 0 + + axiom f_range: forall x. 0 <= x < m -> 0 <= f x < m (* given some initial value x0 *) - val constant x0: t + val constant x0: int + ensures { 0 <= result < m } (* we can build the infinite sequence defined by x{i+1} = f(xi) *) - function x (i: int): t = Iter.iter f i x0 - - (* 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. *) - - (* lambda and mu are skomlemized *) - constant mu : int - constant lambda : int - - (* they are axiomatized as follows *) - axiom mu_range: 0 <= mu - - 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 - - lemma cycle_induction: - forall n: int. mu <= n -> forall k: int. 0 <= k -> x (n + lambda * k) = x n - - (* Now comes the code. - Two references, tortoise and hare, traverses the sequence (xi) - at speed 1 and 2 respectively. We stop whenever they are equal. - - The challenge is to prove termination. - Actually, we even prove that the code runs in time O(lambda + mu). *) - - use import ref.Ref - use import relations.WellFounded - - (* 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 - - predicate rel (t2 t1: t) = - 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) - - axiom wfrel: well_founded rel - - let tortoise_hare () = + function x (i: int): int = iter f i x0 + + let rec lemma x_in_range (n: int) + requires { 0 <= n } ensures { 0 <= x n < m } + variant { n } + = if n > 0 then x_in_range (n - 1) + + (* First, we prove the existence of mu and lambda, with a ghost program. + Starting with x0, we repeteadly apply f, storing the elements in + a sequence, until we find a repetition. *) + let ghost periodicity () : (int, int) + returns { mu, lambda -> + 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\ + x (mu + lambda) = x mu /\ + forall i j. 0 <= i < j < mu + lambda -> x i <> x j + } + = let s = ref (singleton x0) in + let cur = ref x0 in + for k = 1 to m do + invariant { 1 <= length !s = k <= m /\ !cur = !s[length !s - 1] } + invariant { forall i. 0 <= i < length !s -> !s[i] = x i } + invariant { distinct !s } + cur := f !cur; + (* look for a repetition *) + for mu = 0 to length !s - 1 do + invariant { forall i. 0 <= i < mu -> !s[i] <> !cur } + if !cur = !s[mu] then return (mu, length !s - mu) + done; + s := snoc !s !cur; + if k = m then pigeonhole (m+1) m (pure { fun i -> !s[i] }) + done; + absurd + + (* Then we can state the condition for two elements to be equal. *) + let lemma equality (mu lambda: int) + requires { 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\ + x (mu + lambda) = x mu } + requires { forall i j. 0 <= i < j < mu + lambda -> x i <> x j } + ensures { forall r n. r > n >= 0 -> + x r = x n <-> n >= mu /\ exists k. k >= 1 /\ r-n = k*lambda } + = let rec lemma plus_lambda (n: int) variant { n } + requires { mu <= n } + ensures { x (n + lambda) = x n } = + if n > mu then plus_lambda (n - 1) in + let rec lemma plus_lambdas (n k: int) variant { k } + requires { mu <= n } requires { 0 <= k } + ensures { x (n + k * lambda) = x n } = + if k > 0 then begin + plus_lambdas n (k - 1); plus_lambda (n + (k - 1) * lambda) end in + let decomp (i: int) : (int, int) + requires { i >= mu } + returns { qi,mi -> i = mu + qi * lambda + mi && qi >= 0 && + 0 <= mi < lambda && x i = x (mu + mi) } = + let qi = div (i - mu) lambda in + let mi = mod (i - mu) lambda in + plus_lambdas (mu + mi) qi; + qi, mi in + let lemma equ (r n: int) + requires { r > n >= 0 } requires { x r = x n } + ensures { n >= mu /\ exists k. k >= 1 /\ r-n = k*lambda } = + if n < mu then (if r >= mu then let _ = decomp r in absurd) + else begin + let qr,mr = decomp r in let qn, mn = decomp n in + assert { mr = mn }; + assert { r-n = (qr-qn) * lambda } + end in + () + + (* Finally, we implement the tortoise and hare algorithm that computes + the values of mu and lambda in linear time and constant space *) + let tortoise_and_hare () : (int, int) + returns { mu, lambda -> + 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\ + x (mu + lambda) = x mu /\ + forall i j. 0 <= i < j < mu + lambda -> x i <> x j + } + = let mu, lambda = periodicity () in + equality mu lambda; + (* the first loop implements the tortoise and hare, + and finds the smallest n >= 1 such that x n = x (2n) *) let tortoise = ref (f x0) in let hare = ref (f (f x0)) in - while not (eq !tortoise !hare) do + let n = ref 1 in + while !tortoise <> !hare do invariant { - exists t: int. - 1 <= t <= mu+lambda /\ !tortoise = x t /\ !hare = x (2 * t) /\ - forall i: int. 1 <= i < t -> x i <> x (2*i) } - variant { !tortoise with rel } + 1 <= !n <= mu+lambda /\ !tortoise = x !n /\ !hare = x (2 * !n) /\ + forall i. 1 <= i < !n -> x i <> x (2*i) } + variant { mu + lambda - !n } tortoise := f !tortoise; - hare := f (f !hare) - done - - (* TODO: code to find out lambda and mu. See wikipedia. *) + hare := f (f !hare); + incr n; + if !n > mu + lambda then begin + let m = lambda - mod mu lambda in + let i = mu + m in + assert { 2*i - i = (div mu lambda + 1) * lambda }; + absurd + end + done; + let n = !n in + assert { n >= mu }; + assert { exists k. k >= 1 /\ n = k * lambda >= 1 }; + assert { forall j. j >= mu -> x j = x (j + n) }; + let xn = !tortoise in + (* a first loop to find mu *) + let i = ref 0 in + let xi = ref x0 in (* = x i *) + let xni = ref xn in (* = x (n+i) *) + while !xi <> !xni do + invariant { 0 <= !i <= mu } + invariant { !xi = x !i /\ !xni = x (n + !i) } + invariant { forall j. 0 <= j < !i -> x j <> x (n + j) } + variant { mu - !i } + xi := f !xi; + xni := f !xni; + incr i; + done; + let m = !i in + assert { m = mu }; + (* and a second loop to find lambda + (this is slightly less efficient than the argument in TAOCP, + but since the first loop is already O(mu+lambda), using two loops + respectively O(mu) and O(lambda) is not a problem). *) + i := 1; + xni := f xn; + while !xni <> xn do + invariant { !xni = x (n + !i) } + invariant { forall j. 1 <= j < !i -> x (n + j) <> x n } + invariant { 1 <= !i <= lambda } + variant { lambda - !i } + xni := f !xni; + incr i + done; + assert { !i = lambda }; + m, !i end diff --git a/examples/tortoise_and_hare/why3session.xml b/examples/tortoise_and_hare/why3session.xml index dc0139e7f..193523bdf 100644 --- a/examples/tortoise_and_hare/why3session.xml +++ b/examples/tortoise_and_hare/why3session.xml @@ -2,30 +2,370 @@ - - - - + + + + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + diff --git a/examples/tortoise_and_hare/why3shapes.gz b/examples/tortoise_and_hare/why3shapes.gz index 018df525ad04fa02c183c9992cd539081db4946d..93fa28bc56a5fbd5c1b12e88ef3845e4a9d5e570 100644 GIT binary patch literal 3519 zcmV;w4M6fAiwFP!00000|HWF{jvTiUeebWB\$2f)o7B58-h>RFP3?X1kU8kp;#bUAQ)H&>}rnwM>edg><7pcLf%GOmEso1#L z{\$LV}ecyfB{7F7-jlBQv zaQRBj_~!NOHl5w3zdc@mvo%V8|KaiKTU?p>qg#8t+S={%mRZ<%JvZ@s@!a=Qt%`+5 z<|^HJ+k7ZNEQJty>s-TOalf?N-A&!;?*3o>Xi(|#)7M+X;XB-@ySw|{UhlX5;Lt01 zzxy;k{NtZnzYSPnIQoFgcWwXU{ZFUIAN&g6A4hN9eEeZq\$6=WDIB@REDXg!K&n|pD zO-C~yj_%Vjps%Ksn3~vVttmD)mkg<>X>39h-^1qJ&CM^H-Tqg(-O2tQpLX}h\$v>Hs z|8n!hf4O<\$\$(h\$@PaM9UI)!8kx601sM7bg{GyX)=d{k4edbMy#KFMwpn|fhQsD;L2 zObVeH>ro@w)uwjU+#y_W2i}PBrD#hocz9u\$G=~(m!_\$`5#{aP5&mH{HkGE58Rhq9{ zOCX^ZJBevRj|G2Ht<1V(l%sSZ%NrDQ82-LQXkJO~LTl{{C{??%M6Ia=*LT zUkfY+slv6DT7v}U&ORh7o~aZknT8>~+1K4LboB5>ZWa#SOi7}zzHm*oXWKOO9tN5k z!j;LoZs+s=e||{2rN!BusV0x2tG1+8JY`reHL-Y\$)tlPlwY49Yj>RsQzbw7GHRzDH zt3`M>zrR+Fcaspa2b5+cz4215V8c*C+>1myFUM7vm%BB}(!xL>8vg4^X2VyoT<*5ZW`@f{FfLZp|8z@U zABQ}q)|R\$*_Su~fz#WWD=!K~VLp__02AC4{8i0V-H8LTX&By(16a7ibySDk|X1BlZ zQ|&HMwN;V%fYDYPz!PDu9s5?QT^%zZG8@w{\$XhK`)T7K%iyQ?|df1Ql0jM%IW4V@Z z(DDyX{}FBV7=dqJjh^_|*`?c>4>Mr2`0HNJZl74ix5Mc7Ps8@jHf;GgRa{IJms9a6 z9mZ6n*Yo`Ld@2~7CB|W@w9SX9rW##BbR5|lV`TwHBd!`dm`MT!+Z=Kp?FsR{JF%`C z*)O1FKS_x\$CN4gjYFiYgD6JS&LYLqGrfXpJYT)wCB#A=w#h~SLD8gL;%_+B-tMS-F zZ0X(o)4}u3u|GAA{gep%+|gvC=9a|OT3iRlMWhaQYp\$*8?P67LC*)-7NHB{YVUls7 zR+oJQ6*ZG9Irxai zBpOQV)`LHk#xVx;6l3!jx>?+WrzIs5 zmD#C_cJycb2L5+#3%5^={jh~4f4h?x0=h)Cw6 zrJ2P;ihS4|ndG2HEdW0N8zs36I4l~yrU*Flbu{yprDD3GT^<-k6& zEsCy#FqgGvB@WC11rKhY5oQCNu%>2IRT8A7TN^`4022Tce5*Yga-ecRxYE3pBH@~k zuJhP@f|3x^tD;9~0~B62Nw\$IH=l9FPcV9bAQ}sT zSgQKYrJ)L&S4Bl91#jY7FVLgI3XG=Uk#9Lmb-^?+a^G@Fg&LS\$q377uOV%)TFf|9V z4S(9@<0M}&h< zYGPJNEjuVEy}a6kBc`W@h8v7kG&M;`+NcPA0zx>b_=AD_o7?-F-CcVl`}*c5xox}M zZZ5iMkV|qi*?lC|gE*dOI-bP6g-js3rn(=7!Dw7L<\$1U@lg&>ql@>F`rNTa09OI7X z1H(#K90%ZD_-<14V2=iz0D~n93d1;&p~|QwpDws-TpN|TMuy;(>H)D<`h zLeOHejD;bM^0Q3J0eiLE1R@f06jJN~hNp#Mv~Y7`pf~K(ph}!vexFo2f\$a+>p&3DCkj^BNWs}b+Q2;@&nGTwnx((RL\$pK0S{>}=1 ze?6&&ZbNvh?+\$VndKS1J)JNA-\$0k)V4^|_zx`8GQpit_cGrJ7TR8fTu3^LUYTCTnJ;w5F)Xh8+KJa6uN z52h5+>uLdgiW<5BiEadq6MvImZ23eRfw zKvl>_a63Y^h3MG=EwBUNDqzVO+PQ&5&f-bMjTyw73Ff=mWF%`SZvHN9ZX5I1POY9tb#WBScUW6wz2- zWF%DxX=hUz#4-lR>)?aYTsrzYt9gNu1DGB}`xM231)`QZ=1Ri@@D9fKg{tJ zjmS!?maXy5HpqblMTh?7fuG=qCFlzr#&sF\$CpEr|\$#haYemRNjoSy~Lr6uOPTvb_2_ z?1u~cy9cMKE~\$b`m!3lwjZ`X1A&QtZPG*&4@Bd\$l3sm#_G!OcRNZb?)t}#{6+-HRI\$)CCO9xie zM1aH=\$~fRUdr5tP4xU%Hf>Z*=8WFJHI}g?a^Mej}XsPp-`Z>1#g0=ZH1YD~4`oxX)1tH8e?HK!##&@ZB{CPZ)rN@d`y zcU(;NnbD3k^VLQoE9alkOjB==Ld|n02d#lX*%~`yZ-aNWHuFLxe5ClhvoBT)>u_^& zE`yhWO?uFW9#zpE\$1!E&\$RXDH-zC~qy8-o89a0y_0q7XZ1WN}9hSu{-6YJ>?)NUIx z0kV0#fV3o;OX-DV\$TU80LzhZ+btkNeuG\$#Eqio}300bSMJK))wpz%dgVmJ9{q4h1& zmoksxl<*mJAA-Ht_yRLW2dCaqM5Xa4N3x(XxjVoVaEd{zYTvBJYWDU7eBS#KGO(w? zyM#&rXNqyWAA@lEkDN&kbRvx(4GTFqGqw`6z!Q`R*1WF24`Y!I1{;*ggY6>c3i=nM zT1dzSgPpuK7UI-~Iyj#}@{FDdUgM)TXhBiJEC@\$wfBBHong_f`7jrp+o%#l0GTy6L zbh)%fy^nr)Bn4|es7&1}CgleTy)JAi005UF&DsC} literal 456 zcmV;(0XP01iwFP!00000|IL#>Z`&{s#dm!Q&FONa_!p>w8bu6v\$yD50oX8_0z_DUk z3H0\$xHI^wA\$WnCZB\$7`@zV|!QdmYI&5`2I_Oaff=\$&!)`L7KM4?{(^jdV;Z{mLdl\$ zqa&G=Z@mN8sK7QTrK3wVb?4Mg^^T_7=nKMa^gt(iX(OSa3E_BK{kjW);!vja@`iAz zLQ7IQ(n5gord3I4B10)!9klX(aW(eC*mqa{`Ah>pmE%\$0Ej\$E?`hEavRQqzcKz&%I zJ8U*Zst7XgxGF=n#LISXxi*`s\$30O9oK2n3qPyIkeSE(yUo^8!KZZ9xpxFQZU!pj! zEG0^r\$Z_Q*WnvY0ZbBoq2@DNLCIi6QXd8uYyixV3?_cZg{7yqh=P{4EaScdpvWfyo zAZ)UT0%-O^6KpDBt