From 7e21f5706c3f41f677dce3d8e32edbfd42b4954b Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Mon, 7 Mar 2016 16:56:07 +0100 Subject: [PATCH] example algo63, with version using fast WP --- examples/algo63.mlw | 3 +- examples/algo63/why3session.xml | 979 ++++--------------------- examples/algo63/why3shapes.gz | Bin 10172 -> 4309 bytes examples/algo63_fastwp/why3session.xml | 180 +++++ examples/algo63_fastwp/why3shapes.gz | Bin 0 -> 3667 bytes 5 files changed, 338 insertions(+), 824 deletions(-) create mode 100644 examples/algo63_fastwp/why3session.xml create mode 100644 examples/algo63_fastwp/why3shapes.gz diff --git a/examples/algo63.mlw b/examples/algo63.mlw index dda59fd9c..1d979ee58 100644 --- a/examples/algo63.mlw +++ b/examples/algo63.mlw @@ -26,7 +26,8 @@ module Algo63 ensures { permut_sub (old a) a m (n+1) } let v = a[i] in a[i] <- a[j]; - a[j] <- v + a[j] <- v; + assert { exchange (old a) a i j } val random (m n: int) : int ensures { m <= result <= n } diff --git a/examples/algo63/why3session.xml b/examples/algo63/why3session.xml index 1205cf2e5..250f33850 100644 --- a/examples/algo63/why3session.xml +++ b/examples/algo63/why3session.xml @@ -2,898 +2,231 @@ - - - - + + + - - - - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - + + - - + + - - + + - - + + + + - - + + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + + - - - - - - - - - - - - - - + + + - - + + - - + + - - + + - - + + - - + + - - + + + - - + + - - + + - - + + - - + + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + diff --git a/examples/algo63/why3shapes.gz b/examples/algo63/why3shapes.gz index 0338d179d4bb702a682241196494711493130779..56e90735aabafe4a9670fbf558a5995cbf94453b 100644 GIT binary patch literal 4309 zcmV;`5GwB}Axb*9{o1Jnu>D%p3-bwebtKXN4|MS1)b~@hrYx?|;Z~rVe-~Hgrk9XJpQVQLl zJe>Ow#HJ!XR#YBcRU|hR@%<06s)!CJtBR=8l==?&@H0Lgj&^c~$7?%Sm&Q)%qSN|* zs-6s&|BTy14or)9>Z~7w-Dn{ojTE^4sTl^Ie-vT6vRY zLdVW!P^4qQXXb1|<|rO&@~9uCma8Uv_G)RaSDs8_4-ycaWgsP7Lit!NpU3ddDY+)0 z$!m)Wa>_Y)D1XUCCV{g2bK!1o()G8iFQ3oFUw;B6*)kj;ir~FbCQ1@XWs1`2EV&%3 zi?3g9zJ)KJ?^tz_Y*tZZi{7P>O))j2%D`$&!C0h5b*IME_pC;5waJP(yNEU; zk_;S!3OZ)x*vEV4cn4U7_U;RNVsA3a$D=my)^?TCar$ zE++<3my)Kgv#5w`vCT$o`8csl#kJgUsHq(B-OrzPCP0DZstV}UaWJdftEG1~Fo(ks z2P;SLL(zW?T+;zMJOSxPFJRD>MGZB6vBocoa;D#xrDz4$yk19N{6hLV@R2<55%uY{ zR5@a#r8QjZnJYaP+Tnp2mvXAobBP{mR+6e^rBY}pddo}I!>DB@(#MXvbIk4^9G0u4 zc;`Hp(W@F!NB11P1=9ET6x-gr3x_M}APPb2NKjAMgClW!l@_|#^d}vnAF5pmY*n!8 zC_I)KvlUciReOdj<|m5%aNkE&Jc3tuNKg8)!Wzx0eJ7aAMm~_jyJ3h z>dqZpXxdbbEWA9hs+8Bxd%4)OiQ(9Je8l?R8b(8Z6}MA83c{%K;8RuP(?}eu#G!U@ zX1Y9W9Yc?Wt0AQvVa>}dtIlh^_!XfH{h1A3YGP(?@iHRjQnVuGa@4kVOU&ajsUys3 zoNgISZ1XvLUvqV&c57-aqF?@Z?NhH{@^CJD6LuZ*NWEOqu0q0Xa!A>ntWo7}hU_D7 z04o%0?_4=e>5nJeU!ajmV-79}uS4K$vQv?~GC6o3wMTvN>z6NIOB?^~uCLtZZ{^q3 zw_}x?ShELG7=!dS@3jVLmG@erwSh(5=Dk)Jt@2*`+zUQ4d({NZ+hoegfbQAweA#}D zHYO9J6;c}l3)vZ=Okg8*(qPlcem&7c%Tc4}m0XYSb*y_Gn_fSev|P7_+SWWbXZb_) zI!B7icuIhlvLsJYNQ1=}vNn2y4^R$3FQc?P8Y%$vhtHl#0&H!vZ|l#8QXS?2HBcHv zdACW`b!%k{CHbDAlqjMEWmx)zh>*a!YzVcFEF+4RK)zn5n{@qew|`&MH|$#ktTN(w zP$s}CFzOM|$H(EXC5IM&bO!v@xlU+uoiNUILY3?6ygYc%_yZS=PbN4Wd{#(qc@^%I zbcr$w^*H=Jgbr-caaM4)bkl-Uo&lV72msuGa}WV6C94Ra95vwF1OV>}oF!I`WUYyb zG#1C+Xj9I_kW_F)>K2^$(2OZuCwG(XA9DBa5?CKlwm%q!-vE;|Cuu$cm#7hR6k26= zUJA|L2$O}f$>$^-o{r|WBLD4=gKK((KMJ^{N-j9d3&e~HDi#V%F-B#z<{aS!xSk&V zy#(|oul*>{%VabQSHjs~LPle>RV6U-#wusDwhzU%-I)^0qpO@g^mFT^T^=3Z3!Hw6_ww2KYuFlTltASDqgqs zgb|$Lw#5kKYZyUGldTc(8H}Kwb5qSyT#R5a=VmEcO}eRODehadnRN4>j6k@+fr@)d z-o)Tl(#nbKG?#x3p?`!CJPo3>K=iB@a*8b%3*pzWkd}B`3sGmV5M2wd8w(lD#udx- z+jVQ($#b2#xbMh9LJE@5W}S8UlY?;}Q}D&(F(8bwr_&5=hO6>-<^VAVh_?=ZVHWHo zg0dhj1&KD=TfpB&NO-)l%#dP+6fbBj zq+^O&M?#Dul;8rh24@6Ac9Jtan2o+yRDeBe%FcPSduZz8>YIQM>n~oQp7?lp`XPzk zd_h4czo4KyE8KJo9Xsgq3?_Su<`_8CTqqfYpd4U)@1E_ zHd*U!k|;8&68?kI*=l2qQYvea!NX{LYd>QIxjy9fYX2LwX_3<+r$sgv=`_U{g))Xi z42e=w#Xx1skkJ`0Ym2Pa)ELM#x@mON=pJKqTCxyP*ofMpwkU&@UX(vXS&HQP!{A!M z)Jb~DTEpt{2R6u4*|)_Y^=lYpo5*Vo(wxB{>rZW(UBDa~@!d}b`(vq3@- zk)zZ(f%877u*@Szk}=Ata!x&i{P~nYZUzaS200CK8swwj18~3?a~T+YAo5xYO-dTj zoH$2qdj{Fq<9b=1AJ5*VM>;*y7qmCU!fT6$06ui zt*Q@UbDBAq2aTxHY^k%U6#J`;l#-)0Q_S9?j%yGs^&cSE+^DM?_X=232JLSe0Otw% zI>N;qN#zH2A+Y`|vRY1Q&tUKhl!n#hUEECG#WPIa#rnM%Hj{U8JbAZTbZ9whT!{BQ zdDknYjTJH?knkp}j22Q5$OeVd;|2e2hna3}Ym(R`u}NZ+#9oWU9FPUePG-m8kW(<$ zrQ)4=;{YRf{jvvbeX`kPv&m+Y&0hWWKN%KL2B%aO%lk$Y3D|3E6O!QEk1`)3g~?`< z%_f^oHhcB;LL@^DSz+=aI)j!haWtS9B!R~+n{DZ0($}P~Nnew`UVY^RBVEqk`Vv(t zj+SGHNr&vCaEWz4v}~DX^HQZXS3CI1rXi_zE&An!mKgI}wLTldhTjGY?@xYv%luZa zkbv0o8@>j=RVygqW(5U2!wL%L-8$gi@*5k8Avw=BFtL=I|rl?iaq;j+>E0Z-E zknL=ij%RlZoRw#{0A~V!0{?9T-xsh4kH7+gAp^mBui0oRAX5tMzO8qKx9D8~zkqN8 ze**uF1Ap1?TX{NY6?K1;RTQg+>xm1Q#-@ zlnsL6c31O(h96%0_8g`#7XbVHF40$;!dw9Cd2W6V-W1*sfo)7O3g=l0N)}3-n^Zrk z^9+8TrZ7$6jhli&5sdW^BPIwcdH~AkGq@O}H>0(Jp0ri-8xd8)vK+GZnTxcJjTc^I z$Ock5grrX_!qR54-iAP&tuRq%ODQFzoI)c#fwj(SnRNGi`eyg;>RWEp?A>kN3P>qR zMnhitRDN)FT4lwg)AGVmr-v5~s0FP}wTSj+1QkJu97x(?j@e_8jdKReD1(R~yVh9C zS$&WFebMQ4a>)h2oP1(J<JdrjD*w4V-}j3oFkjXu+L`CDF!dDK zXW>`G`3xxkTsY4eWr`xQwTPKW8=0H~5sebSs$Ed!sp*l4?TPL07eYo$%vSoOmU+J< zG@}neX`P}cH&`s_LD#y;ara&89}4)>(f)G*pA-;T4H>`yM&ojb(FvUtN-08mR_?^E zsvHHB6ZI4I-wpLL#Neb7CTLW`XTutqwE^o3K(Rjw_-UCGJ8?g8|JHC{9Cw*yLY;Ha zL2}B9k_57pgX1`IbLvoaEBO&^GfgtFH^3ePXa|Xfao*Ta91cxv#ePOp@itDsU2kWe zPQ*>bJz^dm<_Kh*T0U>{BHQFasl*&u6OIydn_lO-*PA!saQS`ESg-K1on19XWBc(^ zgGQQYJkRWHr@>@`f;`9)DJYwz^HN%At$IYH)qrvTeyw4k3B?J;M-U_D%*h4qoPsEp z_iV-qZ(Op`I_?u=XE@~1aJUE3MB_x`qo!T5kBO{PO0qQ3>zK-)5{`q3L87?W{q-V$ zxxV=7uD=Zdsfz6S(^?bjcJa=1`%V@89ZQu1KDJcu25TOxr9aknmBVH`TygndO&6+R z4_4oG%T)`OC-oO>R{M;=*!Xzuj5Y;vRd6|~Bpw-u+V62#Cp+ZUI9^oZ17y_^u^*p? zt*7UOlr8@;0xpYc3l*$#o^^~NVYDK2ryZQBEs26%a9)QWLv1Do}4faM4Wx@DTr=kMkcoaqB#Z2QTl4y)1ABFnC=MhhH36HKF0)=IrkqG{1P9vz4wr ztX_y;_UhBmsYxj(pX^jQnW=r587WDoP3-&A120_wuchkU=0CwYHp7y!D8 zkoac5zYRazKfT1XlYJ~bv#gg3_+~$!KhoL_`u*wsc;x-K2YvW)?F{$y@_LGJ6?QhX zmjKrrHcv*FDtb+wKYv{pJzw`LTL|kcT9wV6+Avs?ZJ9igdq#Tk+>HfnzkRUQ;|ht6 zA5h9Bm=q-~!elkIV)mb(_+0Dv`n|qi-B5g_+}p2#Ve zk14loB81E~gLids!Mv7w+4v^&7+Jeg{&rw^(Y+KQ-@Y$5&$+JPJXkh z0d`fbDJ;sg<2owTvBDPqcFw#j2OKw!&^1(=(Q+zv&1eJ1y6KJ4>abX(4m3rxvgUnGo zO1GT>f;AcYA)__Lx*+^!cc%g1Y^5h(N&;+vvc~y)mO+QauUrRZb-1dX$z98JjJdcL=X=akA`pH9Pn>N)pElIG{``LKIfbt*|5J|w3~nCXM2;=U7C2u+$TOKyqKxg6o;Cc?W6qy zUeBX(0R~UT7#>eXiRJqu3D3U^OZ^DyXV@r?2=|T^UAiFcyW}@BXa$lF7WuU!`D%er5 zY~V8q!I{fY6Mn~fzX7ie$HfM6wx~ru&P8Qyh%avg&cM~h6w}S0I%4Zf8C>8pD#azn z^~>0+nxDeLhRPyIhj(mGaB^cz2>4CTm1chbb#N4K4ss@Xcp#d2DKvp2XUjs}ch@r} zyI_I4A}vgft0gV$e9!Q7(UvN%M2RNO%Ovb=lQwSEj4E!QpU7~jNQiiXs-aV~X3x;l zn_v|*$ev}G{l}0AeGO?a7OI{jpiQ3CZXux)JK$`ln1}?GfS1kbUV?@Pg9jXeeu7p6 zpC*1DY6on1Yvle^l)wRUM=i^UF{|p#AgY+nU6n^p(HnLmrZ89dW>e1LHop3wJ86u){6!6<(q`xagq2;5&B{HmY8dgWHU5CyCk4d~oyzI~-qlBggd=V{i1% zwAPAS>>a++fl9#g=59arch_irMj`kL-&Nl-lqm?8L__maSy(v1N$3Y>8qvIap zmSutU)Q+{-=_CUDbPx1uY-9kUR|#yRErp;$!M(%Reyos-C;U@{GtegLqoh^Fg?LNN z5elb-E8^vcF_wBGQS|NF-jCatBy?@^&SSvsJ8rtHQn6wr1{6|rf*TIiFeSv3% zty6uH-qy$#VY}M;H-a9WRbEH`v*pq@scY7l#lt!d-4?v*E%-#X&X$qhIxV4(y*!1>P{JJA@D= zU@f}_sSV`5b`}%Wcs2FZ9En#S9}qsT_71^toScrY=;FKDvz>y=YeAAii%W7pnACxn zl#(pc$@H-2MsP%3oS9!TKOLX8tj?5kvVeve%v7w+c*F1?FX?{9T6K9T)PFhIRQXjH zr4>U`H7txrP=ZY*gg`fJkPXJ*h&YDPib3y`&%?jw6?xpU;cK4X#O;Js1f#A zc0_h$I)6lqo7}Kui8z~$ZW+J|Q_>|2Fxuxw_MUI{;eS2kD5vmlv==3kLZ=eee;n^m zQ|6LT0>&$gLBd$sAHJ5OTsB(JB^?leXU~|ZVMCOK%aTy|f%Zw&I?Pqy8P{9$NJfw+ zeO9ZNL^2}8H?%JgawT?GHhxgxE2wsfm{aTlO3=UoQ`-Bgv@!{E(0T09wE;qTW=QUr zE}#xhyK}f&0R*wmUs6RqJ%C8{`EU87xd>tdQ5)BtJn26)!u0;I)%0i#sQqCpviK~f z8L+E|A-{rIiQ&j@sYXgq!lbUr2O);0X4Xx6I}vD|R&1%dn+CNsj)=VNbO?#_KnA}- za~L))sbLr=Q^b5$|FQQ9QKPm@5oG;YS6d>fp`lzXB(0KnmAol*`y{V)wCh9E%*SK7 z;u`@Cr+h7mKp%HFxdsRj9b-`pP?DzQ&kEPXwgw3JNt0auaK0OH`KEGy^l6#ScxcqG zW?`>PX_%lwj$o3Y;!pz5a#XssBZqxcM&ko4E@kec3@1AC*u&nIVjVo7yu5PBhanGb z*tt&dgENC4{h=nTvlT@o7q1Zy-us)k|4pu<{N+(ioczNE|H(!VPEk^`{>q$G+W3)q z_U5|`+#vW^&u_$E<|4<&Q;}Up(9lUJVw_T|(3u?@ZzmP}UCgFc zOWWX8+JoT|zybT$kSnWLO%-~Mdw~TGsW>#xzLyD%C0+DcMq%0sgf2DoUqRN?L8OeH zVkTsT94ke)i9T;sB2&eK>$cpndJ4pycPl%U5A0&EU&QW6^2nkAkiEg=9h6q#43R%M zltlBCVfH04KzAlGMRsmsq8V@7>c?a05NRb2~}YJ8f;bxj#&{c5z*?gWf(U@APzyrp1_0`NB|Z9%lb zTBfg4YjXp|XJbr>nRnOmukK(1RE5n|2rJG?b;5|$O(%Y)1~5VEz_lPR+2M)0X)ojm z3mX4GR2nZ%itv{j0_5ZgsIF3fZ$Y-fTV}5_HJETXPwf*uZ~kRb@|DVBw7`xy8%*|x zaP+vs)M6}M4l)ah6V?WC8KB!qCn=6l3$Bp-ZW4a4>802o5e;YX{^zI_cuqoZSG(g+ z-BLKsu(0&{ec3fd($jL@G^A3(SOFAxP`j#rN77z|XFJ5>o^sKCpjh#v4(oJX&4z(_ zO#KYor7R&ue^kASVfe8{IFe%}vfJtmNvU?Cez$}8#ezW{c4bA~W))F~cJ(ZHRyCW7 z$TgfC#DJrc=94Xh(hFK#j_8b~*bGvD5R4)u-HA~{EJC8XrfrPu>RA_1fSEohSmOo!ZmFXsvzc)t?b5rzQ=b>6K)xbSGE{jo2mIOtiNMc_z$oF=YxSMLEBE7>bz zv=BNuGZ~jz(7`$^Jx~(&R~n@CI;Ulabb&=ZrbYHDqXf_t3bDop%49|8>2KSjb=sfx z=#iWJgiH7#9V$9Xol$5su1uE*)GiB90e$e;ZHtPXp8=J?GR`6n4T8+-imb&>e-ExJ zgvp4?*zE~d$1d385AQl4^Fwg`e<#YC3cEaRnkF<$5L%p`M z1kZr7H&9#eBX)?6U256V%V^5r{j_XY>`z*TLf8MR=Ha%!kn6Tp&i?F0C$fIi*S)@R$%CFsku`kpArPQ~&sycIArE4Z)Hms;-(V6vD8miV9vTIh3AFQ2I{!dYunWSI83V9IBSG$h|IF z=R`x|xDK9`jNwZTCr3T6Y?iSnlx50N)Yy&5!k<@>?w)9F_#1~ChxH4G2|m%8<$SKd%@H>=aR4S>sayQ! zDqJ`?@xE=NoXVC-bsqapPIf#0nV-JW`be2O(=ss411wu=0omk~ylym-oc6 zn>{gt2?7ZlU^@ZH82L>J3IAU!{;e!KEqu`ZbR4_mtVYU;A-4a4N$$UNH$( z;`a)Kq1Lq+Lw8f$;--uytpHH|PR0334x^JeW6_vMtr>*oKPd85g(dT;L2|`Z7k}Z8 zl%&@6t$#AdQ0pa)`sW`;&7I<)E^}yQ?w+^bl1j`HTF6HRK@0%bw*j$F!csBl`xtaO z%>t+=3Ixv+Wy^h7|Bg$Apu=Ky&r2&;lqIBlnua?nnwvsuT+vs>caVh@Jh&#F-X>~PdsNq8TnIgzDh zP6W_i-Ea?$_P67|TTp1ab|o0i~7;gQzhku#%K^%)K%Q}Oc?qgF;CG+A1V zQ5VOiKH8>S)gs>s1Z36d7~~j03==jHhR^F_BeQ3}LFuffvC}ug!R@H}s<@g-izcmG zz4W~dN?Aq&JZW0Q%;=6{4)O_#_8W#t(}|v5q2Gev^;RVJKme=GAh=`(OH;CG3yWCF zY7d(hrSD|?QyaEp3L!=}R@evpUHq%3<6)e63j&6W=n#Y?(o8o0GgFfx!Me*K+iDdV5o=%pkM z9v+SI@T0WtLx5}Dp6lqU7F#WGziE*#@Y?x4o=fu8oRPah=v9|*uNvL&d+sEXJ)b|c z%yu?&IfW)xpyULX{oj?2$ouC*4a2W)Sf|OU0>Vz$Mc6CH#cep9oXW;@ig@W&$+U=@ z4xR?KU6fIA7<0yePT3Sz8=pWA9aR*YEu`LIbZ%U{{-*Ipzwkz9UL9~)!c|D`BTgPq z@3osEi@U!vF3tvl3y}s7aTT9TO2DM$A|(NGty#@uGAS|U*IA*3gMi+~ghZ!XVrnPX zJu#sVQ&khdJMEg(h7nU>AsE7+#`lZBuMI?^<4s9)AEKnPg^BNZPYq-=ytvISvjH3? z?&~(B!AG3jbIT5Y5>h6J$EW8Ckl?)c*S1fQz;7CyFkIxwXmLQG zY9JCSgRc~Wh$q*U1%b!w8Z^X@!P~s7`YEs;n{1DpkKi*O>qqCuP1>tpTFAqb{Z{Wn z^ZRwJrN;UPli%~{<42{ry_&H+;+i{ej*=k?a@-$Dsq=YnN=DNY3)z57fw#2T$ zrEHXRQmnbsM_uO8PwT0l1yd0ij>&8C0#?}eyb{-%JWVF;5|P4U4HVtA1%y&NpckX< zx$GC%=M!QG9Q#S-j|Nwe{eB+{v??F3xh6XoUcJn?^YaMQd9JCb6g19V3U%|I`@-+n zCOprKF}GV`iCU{lE*|8oqDy*tW@XzVQl&+4!M2J#zl``X`Mq9#ID<@5l+*<>Lldx3 zt(XRLM!-i7I&*F&A551<6HqzGH=!DVx1g+r^=5hwgl$=<<@)cJ^iAKmIt#Klt^o9& zq&36rgmG$}r>mL8>*sAJ10B1eb>?#ORZ_+jr+kOT$IQw)I2B<`6Q`UH)lXJ-8?VdD zO?D=4G;UGQ`MF@o{0v({XM1E+!6m7z@ZD@wK?Xs-&-r#R<-Cw5U^?7hLfy=)l|cF-q^ndB(W>Xz-8qDww=6wkoYmpzLwW{2t*md@T-0QA z609sVOAp#j*E)MQm7EC`jq@;(AeLvd!v0R?43EECXya>sT>K3r+Ppl8&YiN9WM~(bz15U5aM(%f@ zl3NZ+XZswHnxDi1kGhpZlj^0#B)846j4K}~CKp8B!q++_@2(~A^Q8+^c_O^OvlDDMtP=jD>jb zgzPIbZ`L1rd!bAB6}ufbxXGX;u#)JZeHCGL!0razNN2!qN!zKN*mdin`1@9wNAtuL z6LGHil~w;GFRgd_#8SAPFpb;FvN{4^`-I!FEgZzdlW)azT4PNOws>*`xhY6iaWNhx z_FMj8W#sF4qQ2Jm69ySca({`UF&z2`Ld^=XNEmVq+-WLIk}$bg*d5J$XG0a81Yt!| zbUha~i#n`yF-7v5S??Nm4@0RX?#Y|xIj%$5gX}SLne5M$@KSh@$ni!Eu+k4=ICbqF zompQaqj1>uIsWM-)K7ARm2v17o(&X+h~D()Dy~u!ccco}Q+bRPwWffbB~sLu|8smu zVfl$X)TjYT8a@x}=}6GLVTA^CCO&%#By;ZTO*3|^d2u;soD$1!3!iJ(Tu)Y29nW=g z0J4yfs*ECxX_qr|IoX=a&+~s1#ZTx+*O2$evN>(kVkg#rS_D|MbY54290(L`Ss=cb$8sYI)W8w>-1s_Wt zS2@4aiJV>h66@vI+O$R+ZL|+3d&vFNwzBJgKj*I|2Q&+(5GgJ!VQTlPQKHq+f|Rar zx4USl5(wRJ2!&kvh47!HX#~0n^gwicR*hC63bheE8L~iW*p1XB2f|k}(WSeN4dy>! z0pm&!ZnbY~YrnXJu{xjR^zt_ETE^0AUGgIrG(7E7=ovGzQ(e01{n5cH_f)L$ZWs(| zgP!wpBLESz*Ia(zI*Fi!RM}YF*?rzE^VG?m+U1JRdb5XD z+Gr(Ykg0bq@@3KI!aKXv4;Pvr~k&{a(C>`!l(*w9vGsv)I{Xmxo< z1&s%QYD&3}I-cunDt{9@$K3I`-rKWGqFJxkxpudIO3QLSHBn<_z-)b=>T#dslo^!6 z?*HX$ePMgCAjGlMH~IE4QL*g?d8TFg{j2H$5mwy_dHtm){}u;Lh7bL0#5OGwN=>*` zSQ2{)B`nTESMhPrJ&!`z<4aaiCy<3_`Fu33KX9ROjhWHg-RVkcOM$n0w!h(SMD=xH zz-GvA_0z|qDJt+eThDxe-{U)-hZOB{N9&At=ik@)cXO_S?h9MY+!`I`ui8Lgj~C{P zOz4M=jiS~yPJ^vS#vc1!XHEgmSV*_nKKY!Qq)P_#o=dm$njq&Hw}#5Sd$QeIZ%2qjCpg%&>b1&m<|)fBH-je?3lS@a0$J0Sg)ZvP=*p=HUvN`O==gPR znD@>u9-lfjm#6`^62<7BR2*1gKdI>Yu?`6%fd?hUM~yx!t5XZMuove$dHoy+$RkCJ zjq%XyWQ&d2UWSj2G0?wv?5V_7609e;0>wwq(Tk`P)A@^B$9weTu?n@i?<#&mb=_7B zlW}L|o;R$lBRu(8fch`&H&b9TYyu@^p2HN0r0$drIcddis9~?kYbYg{3DeBs_+oXp zM`7Jec^Re?kOsdvLm^As{RHiRHpn>AraN>bDI8Ik0t5NVv(%j| z>cFE-1?yP7<=-Z;dPgH;^+*Z@88}gTv{XDWYLBhVxQv_#WvXCWSBxpI_3jIz&{)XO)L`MSVVG6aR1fP z#X48M=!b8XE2x7Ip)UcQ5W(@77(qf<7Auv4j2koXzu1|4$vuJ!6oW4HXB5*+KqpNp zaZPiqI@Sp07ip=4{VI=oRkGL@;gs{YuJpK7t98?}E$I z2QYoZCc)yd?W)MG5~e3=?EG!IBfKE-e1G6%mKzw=9Box|v+py{7b`qZU>+$Oh)Knjd28hU(u| z))bJ!)kQpAfrl=c5?B5<@1;P@1d9*oWjqnF5Qa;`)LD zC(TcDNBU)oLdFfWkJ9W`7I&HfY}@B+m~e8fS#y+4DA1Vqk&fJTmiYj1j;$bLUkc4Wx~1OJ0tqO`|X`?W|JX1jZ`7F z_TZ1z-#FZe^WMy9nt|9>9j6noS6yaUkuH)MRr(3t@Z%Lz$Bh>iwW%jr&{`ArI~U_! zlc06_eJAg|rG*kF&7c=mG(h&W% z2qQE`6}c+T($(RRmkeDOhr|ngZjJWyqI(-PL;%kpJejmF#L#d-d*-?J&^e2>ltizOv7NdQ?LOPR>fDIgu?tY zLa&cyoB6Wy-N^%*6vCoDHhjV&aBgQ0E=oW;1Z%`NPC1*A7#9{yR`lcMjPn&-nC`ma zhpo*j_gvpb2!TxsxqXI=Yn?XCw6mYU01yiGVE{A^ zJRD$#RQ-T~ffTgd|HWokR0UGPXKGWtZ-^C?)S~D0v~+6sy!wknd;a0OJd>=WkQjvM zeav>d>JEZ1pG5zKtVSR-d9KnMkaP!M*Ly!HiTa2<@iRcQ;*+uwHR5d0lz_$>8aHJj zaEuJ2+s;99@Ob?`L^Qr7(gyMl0m{f>SO`Jd3qwi#tAfsTv9jMxS+QVn^FTyZuq1oRd*8GmpCNi(?p|f+IGC9MKr% zIX&|>HC>qD{#;?!^vZ!ph2SxRm>UR9j<6Cn}^OG|!I#gr)R0feis(&M%~6pE}>jb35C>Rhj;2yv=q+y-`|&vB_r~9s%jYlSvpgTZKX)&ra<0UZwckhJoaz64-bho? z+oyfOjiQrw$xGzv-4Dh3gmbBBj&$R$XI;uqb5hCGnr$Y^vNh6Ou3T@$Ykt}R*0a-~ z>r^!E^L)`1zpF1VKG=uIIZiw0SW5VYxrA0wtALb-r~y(hI)T$n<5wq({;gHkEjdL} zKP;Yb6Bh9{7TlrQEKELZ2>L_|G?wZ@di9wgwLSTfI;TA${We7{5 zHkw}gEn|KS!4Xw$7A-R%h8*h-H;wiHP&ixn7;lx%U%MJrohdyGs6s|pG=`u3V-qN! z4#iVvMZD;oFnlDZlYkTIMP;t%BaSqjAJ_2AiU?w=@arHIFK?W!n^lD-skD?7{64a8 hEqlrLB+VIR$vO_4kRFh3RL=ZB^AkzyVO)cP_&;t=-q-*D diff --git a/examples/algo63_fastwp/why3session.xml b/examples/algo63_fastwp/why3session.xml new file mode 100644 index 000000000..aa0c8c838 --- /dev/null +++ b/examples/algo63_fastwp/why3session.xml @@ -0,0 +1,180 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/algo63_fastwp/why3shapes.gz b/examples/algo63_fastwp/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..1a620014d8d52ee8580baa2ec30186f701b00465 GIT binary patch literal 3667 zcmV-Z4y^GXiwFP!00000|LtAdZX7ofec!Lpdk}zC#VcSNFoG3eV6l0dm&GFBH4%_l zhNJ}Ezh826X%@SCG`2OiVm0E}!)B8#7SB1nG@C6AU`R2A2ofR?WKFIVDFA&=0?&3o zot4Y0v-~ms=HLIC{fB(@$DcR9T>lw%VyAcDFW#4nk7qyZFv44Zf7?EecJkfq%F;cz zS-keY=l8$f{I=8gKh)cYsQmlQb&a^rH@834PWnGCKDNmJ{I}*r=lA!%sxf2wSFfX3 zC`jG^5JN#~DyU}73X)wxG)uoPh!#xYcgV-{c=r(6$sJB{JLps6Lh9;Mem}9C;rt)P zm?Tmm69SU5!Z;-mP4I@u1*y+2-lzPr{(a`JuKfSb!sVau)ActsnT!s$$c$cjUqF*d zPWqyXjYTE#n8|DHuz8u8oXAKhgM9|{i*cpZ{VctNK1;^3T?G4V4||dn^3Y3f>b>FaCvSbTD8=aKGWnp~?IXhW-DuYl4 z6nYI1fKs=i_Ox&F4juNZahDszVh6{E#s(PGhC{D#MX z>C z2I--iccer2@Jp|HUUJXN(erZM^NM+1&CFNd(DV8WJ>R+ZzK{H|HbCqn%#^)c=&$f$ zK!!Af#rh)3Z7kM?P!mI2XwjRbSM{Mqae*Kv5LCr*MImZZ$t0qN$S@blnMTm8PE*07 z60ppwAw%rc58nI!KH~^`yUoINtbe+EqFB3U>Mn`5?Rgi&8+SfTrUR`z_e9^iq=)vb zbw)L~VB&f=Jivb3h~qeW(t~jzvM=u4zZWHdTG`zYy)SyaQvzQ+fgVmR8+fEn{d!%^ zj-RIM!$C4QDxPp0j2xRFi7fLNK-vJfP&&h!V*ratwTf4TdR)VZdzWoAbjko}wpq z?xgDjw)gu=1h+~tJ!>I8{8EDXd>nmC*J0@1lpkt&9foF(u)WKqWvy)2Fl67cBx{)~ zVD$l3^;RFoML9~Wv@893%^6wF$W*oEjI8}ebawj6^IhwwT9L$Ht7w3&qIGK}vsTWm zm193u6Rq`A3zd0(`(fPC ztcfd;VNI}tH1pInaeVb@Zp|5Kzj)v$=Vd7niLT z!FBW`Z5t8(UBM;51z#r>0M0wC;^#erH$I9AGaF|;atE$YpZ+}s^fq1lUZAIiF)~JH zNLUvDwb$sChGc@#&YH*OwYWB~WseqM`O(5-iqb@lLuo$gc@jKt&mMhoN)?|_ zX;BcO5U9vHFJ&nSj+|VNmO%GNuHSjK`bh3hihElRkl>KE@oj!5B*7??BMHS9T}oez>q^54(;lG!bR-(2-ABWhk*5VUNnfqFyO{? zZM0{=;;yenvV7Je#Wtlls%P7#6cbsjcS`$YvMnWRmxRt4oWkTYDnsSb)#!Ui#rE>8nQxTUUxTt^ zk1p!@CqMG*H&PWXeVz4Td7n1?{{5UnClXB7-sQb-cCyZQR=l zY$xcrKN!@;$c>R3BadMuM$$nO`8v!j%GSYWG*Sg^yo5d_t ztn;~~b!-PB0LrX`O$I`iK3c0qTJ8pW2h+l$7k@jVV)8pC){RLT!ZH z2)PmRXhKGpr3+DMiOv?EA^T{wqLMCW*2zmQn#1 zGNdSzRYg06S~$evgsEkr-!}*F*ZaZt#|YUD(yuvU_8^|l^m*`=o_M&734K_D;eZJ1 zxd;#D}|5Q$=)V=&sO%Vv<5R_ozxQOl7tOpLM%oXVLaGH*_*4urgNLlZ92E<+_TlWsJ+uV znqUc(Q>o5wgF#(ll*M3sUby)D;(!LV(8xx2etIE9{$U{$gAk%v7eaPy9l}fqVH3h< zCxrZ52*gnc@oNYnJ2wJn=SJWO&W%9+>KqQ|M&SCn5y;+m!|~h*e9`AdNb)HQ38|zQ zJy5po-I#2%ZTk(y_%P$M2VG!SXg=0 z=#xG}^GvELA$T$-6jf{Ml?@_@0>whELCEI7I~)Tbo=JsNal$539OYa)F0awbK;WDY zMrM;A-5=jRpVU#q4&NoR&jqBEq(VzUhg^TC;*Bm^k;zI*Y4T!4->g@ZQ?*v@*;G_S zAxb3aDjiF}S~pcnds$aTkw7l8k=K)L=lsUXk|I#$SgldfWQdB=q7JrdjmSFHeeLt! zrmy-bv_r?s?|Z}L4#n<{IbMF=G|&4}XwL*QqRKJ`sR?yuxzI6Jfp(}gVzdy}4t99r zZ~aYXKhekjHgtX$=*%t|SE!=W<|K=&B4z`KR541@CR}?h`?R0DoW}DTTsOG(Vj3+* zg#nPjN2#n7#mWpMwIrkD>Sp!rleb^|$=h#4!-MB+iPckP?NNu!ZZ!P7aj=N{Zzf5Z zv;!5f_8HPy6?IgmnDK+|2R}@`5pN^jM!aM9vZ<)F)mq24%x@9~p)!RKi_<0J@}`d2 z*W_p4uphrBFV8ntK2ug6Jatv9o+xLJI#6z7&D5AlN%?G|7uY#Hnp>?>da7EQuU9@Dcfi;flSNWg5EsZQ!=}7W97!m zjg_A=aZJfYOIBrx!llsqO;hUh(UkW6V0*Uv>8xB{oqh0EH><>y)f1+(i$A1RJG5tB}tN$qklmtQO=(G>YwC~zs zaw0CSe4ogcQt?luH3iI}sL;;4hirY221*3KwygQocrvVY&44De0w&vI$#N*I9Lgg5 zb^X17aU9J~Wch3ueR^Be0Yg@ZK^B$jG}{y?-sETipw6--^xi!G&G(e1$QmQW3 l4x}r|1sxQ{Xk3X!lw~qJ?+#*9_Af%j{{amhCmd~>003ItJF5Ty literal 0 HcmV?d00001 -- GitLab