From 588edddba7bdc303012c73e76d50ce50213d7515 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Mon, 7 Mar 2016 15:33:39 +0100 Subject: [PATCH] example isqrt: additional lemmas and assert to ease the proofs --- examples/isqrt.mlw | 8 +- examples/isqrt/why3session.xml | 166 ++++++++++++--------------------- examples/isqrt/why3shapes.gz | Bin 1310 -> 1448 bytes 3 files changed, 66 insertions(+), 108 deletions(-) diff --git a/examples/isqrt.mlw b/examples/isqrt.mlw index 3b9e78b08..f82246b63 100644 --- a/examples/isqrt.mlw +++ b/examples/isqrt.mlw @@ -7,9 +7,14 @@ module Square function sqr (x:int) : int = x * x + lemma sqr_non_neg: forall x:int. sqr x >= 0 + lemma sqr_increasing: forall x y:int. 0 <= x <= y -> sqr x <= sqr y + lemma sqr_sum : + forall x y : int. sqr(x+y) = sqr x + 2*x*y + sqr y + predicate isqrt_spec (x res:int) = res >= 0 /\ sqr res <= x < sqr (res + 1) end @@ -56,7 +61,7 @@ module NewtonMethod = if x = 0 then 0 else if x <= 3 then 1 else let y = ref x in - let z = ref (div (x+1) 2) in + let z = ref (div (1 + x) 2) in while !z < !y do variant { !y } invariant { !z > 0 } @@ -79,6 +84,7 @@ module NewtonMethod = sqr (a + 1 - !y) >= 0 } done; + assert { !y * !y <= div x !y * !y by !y <= div x !y }; !y end diff --git a/examples/isqrt/why3session.xml b/examples/isqrt/why3session.xml index 3b9622bb7..483e0978d 100644 --- a/examples/isqrt/why3session.xml +++ b/examples/isqrt/why3session.xml @@ -2,160 +2,112 @@ - - - - - + + + - + + + + - - + + + + - + - - + + + + + + + + + + + + + + - + - + - - - - + - - - - + - - - - + - - - - + - + - - - - - - + - - - + - - + - - - + - - - - + - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - + - - - - + - - - - + - - - - + - - - - + - - - - + - - + + + + + + + + + + + + + diff --git a/examples/isqrt/why3shapes.gz b/examples/isqrt/why3shapes.gz index 1211000f5228b306b24725935e87c3317ca4ab98..10c2d35a2b0389a436240082d4b717c7e7f21c31 100644 GIT binary patch literal 1448 zcmV;Z1y}kXiwFP!00000|Lt1cYa>Stf4{%N&sPpc(tJX5Pzncz(!Tk%Xf!imXp=Mv zNB{h4o%8P4UgwhZ%w1q#?A`g0G{4bL((G<+&Nc%ON-lSk\$\$Um~}VxXt^T*!xB~0r)eyWV^G^C^kLHpgacb}#un^aP`7_vhaAimb2?Yd z)S~^P+M\$1Nq|g|Gq-3nGE};mo|;m^cx+A* zx+)dwBPM%9N|n3H_w}`u__49@oFSsM>W?{tM`wW}JCjr3SaV\$6-rPUP&2`y6dc;AL zSpR-8yOR34dMKp;>cW*;<|xL7+L*mg*hjCwb>67fh+TIk3WUu>W#xzR(7cPz)DWBX zY+WE=G~Ak|1|NL1neATkE-Y@31LL&I`>osH7%ty)*?t~IDKrm%OxWPQec!a9Lx1V+ z9`PBmvlDj5T^\$bx-%=H\$e?6)r9WvoO@N&AbecIH0p(8a!AtI`grk zzaRS5rO&DvO?iouF#-M\$lR6B}%Np2e1z)RqbAsVy&WGd8ep2*|A)P;-H|4CPnV5An z_r%|K?X%Jj9Ca4\$-}a8#\$HY^=g\$)Syv2ZhGcI_M^>MGwU@k_}+EdDR@?NAY zt1jOHyxC5c1S1Rb9+X@)T` zLxaVN\$J~6XdgTgY1{;%*2lfG;uX>KxFES-npF%SgU8>f#noQ6-ri4()OXRxZd#\$s( zD*F;aa|)E-DQdn5G8Ys3q\$QqM?~*S?S(Knvq1pglJcaBTIcdGXyXPf@=1AkM*kYU@ zHA>NIq\$hA1L+0Q;R}`\$54S2-{h*skgeQYs#g6yTHG91}8Ka^mao%8Qk)O71*`!2G5 zRk\$|sT)?`_1`|>atOW)laiM&&eapG(4WFwzjw~GfVL0fms}UhHW_cwY8~M9l?8Ya@\$^qNjO-K#p_u(FaHU*Nty~wN*?71ZQm}sU;>G(FURH z6b3RdyV|dK!P`g08OlB|Y09b?f@x?7y)8*F*3_Q*f~#NuS8#e;nEVGXnOn*OG5`Re Cr_\$~K literal 1310 zcmV+(1>yQ1iwFP!00000|Lt0BYa>St{(is0pRXKfH1E(9O5wmz`fU zctekWJq+-CH0!B#fWiDcT`>&s`2%1c1&GfUqH)9`\$p+#k4iH^f4Zp0~-NS05vYs~d z{PX+cy|4HOcrL@PMf)eUW4}uJU<^6&4gxfC zm4c~=NpgygC^l#>arjf`O%?;Ybr%vgao8E9dQ4>aAT<((R)7h?*&qQ*&SY~y1IfD= z\$hh1HK\$N1IFmnnvNKB7m5?3_Htdw1b_7j|MlP2xS9 ze#*@>ptE5&c(i5\$%psUQj{ORolWHbYE>SYTx0}@Y;Iyof0gmylnujAF?#%gg80@p6 zXAIe)=!_{RCC#LigSnmju65|id;9im@5ViZX4P73)Ii5FTlm7QML1)v9Uf9bu69C7BitTClALbSGIU`c2*_-Kq--QPVv@!f6RJZ;ep4WKtBT=n)`AT}@6nxEi\$xYBi>\$#nl;;W*GCms1^^+Qo~%VO94Uv>+A?N z3T#B=^{VGm%0;F?=H#5k\$}AQQ=2Q!E4zc~yym--Ob9vpeC)DUEQjmGy<7K|7HcV4xga5BP#=e=2OkS_&~4a^dr#FP z>m>kh2!N(0By^2S(8ORVsr#J=ldz?xJDoXvzoDF5FX6jN_&8_+MiKAv}iZwxWrB))E!Nzs7(*l\$C2\$S)lj84*8*aS)#BOp|t8EwunwJ-;h%i?~? z==oqQ\$a#;*(Xy{LvQ4XYHbS}jN({yOtP7C-omqUYQrs;ld5U1HRUxvFul;V3O@)v%4GV{x9tm67pg8)z0R{>1__*e2qH#=8->C#S(inyQabZV U_0WCR`(51YKZx(EEU`5J0L#;iIsgCw -- 2.22.0