ࡱ> l( / 0DArialgsupoptaTT0ܖ 0ܖ"DHGPSoeiKakupoptaiT0ܖ 0ܖ2443 LPl( $HGPSoeiKakupoptai HeavyVer.2.02"HGPSoeiKakupoptaiBSGP22%cIfd<*+T-?8,M)llI 6ɩ ڱ4n18ɼPSWg:dRlr.kOG+1 TaZ:M=RIFӐ 7ze~OJHI*" #ifkNƵ)WOMbN~-QBXHTG[vŊ fpoL}"i |K =*P;,yZ,#þ El&;c'{:$6HKrh."Ů>HgV̄SB>L4ȸ$T;PDbx\tcc̵`De=w=F`ИSPM|e} stZq+r]H$IZ%"JxRq%-,t2IK4D#FG6{zP~B p,=dW-ZZ*W W!t*پ^~$#ľ dv7]R6*+Fu X*hlH 3gv qpi%LIKx J#Z,؝#t8liGR"B%yˬ$A,>~aAp `=!)QL:Fp A q$ P 8E5Wb6sgv+7n%z3dJVlfj>](]M5{/LN^իOWQ6vjV-dԽM];/U%T̴4LD h>Ŗaf,ŘIgl94DԚ&Vja(ֲ[ku{`l-`(6Hf2([km,tږ[[wM a%Fޛ&;|}7|pN 8NeDq)88܃IK场RsNcsrWsKN-ƙ&StbRu&:7]2L݄٦M3h7khx7 L Cw}>i?'q@@ AA;,M#B6#PPPSDztPtP!E(1G9H)B_Sa”S]uI"BvGpXEx")0~? $#Dq  Bā !8H DHDS"H'%OLaLj^LJz5\ RMi7⨱!0PyC$ghB#o K8Z5L fn=Z;m Qح Bu-{1¾ݼxZ1#hgI#Z(L$7vHn<B;#͜yyyGoH.)PECG"HԤ}73*Scݱմb] J¬@r3U0]'oT!,m?Ԅa >JϾwJ_:ߎkh ͤI2_.q8V5=fG5$rUi^+]Βʴo`ʚ:G/oe.Hk{^UY,gO3 j7]f?로 D7±-E, -/V jIMp:mrS]dTMY{:L8wdSǚ$1ҬKcl3XG;}Z&eX:pdRaySvcD%*!Ğ:¹aXMuO)*a}l[7URo@WoUA~C@BH*j?_,sA97nXughnZ; ?b]Qps&/ۥ[Of7֓ɏ_R_ñ/=ԵGʶ#HBwyfte'l @iRP<ߖ D=8!}L(G4A1 vsٛ<`| P\R7w P0re JV|xYGsFǑCQe!_G6 ibŀh?Eˋn\ oPIrm [:/C IF *0<-pC @`KGfKPn| yDWAWMG- j% y&#\ffsT%vEOXb;jNbrKq3sP٣9&iiIî&( 11n?ԟyL⫄ЈpQ-a 62-l7Ls }I3j">%/~: |] "sGwgrIח-^ԄQ<2a ;~a! B0:`/dQ\ŁQ٬ BRޱp`B MV$Evp߂aB@ch-1=MפЁ3xi[Z>3I!r؄xCf 3i%,>.@ ug7E挶&@9(.< I#KoxӛּD3H,7Zv0+F. l vOD>~xH ,Xh!씷c'+9>|riF_M7#Xu7h(S z| mŘ(Vb=cs3"f&2^As_,4pbmx\l.Vë5tqq$J H18z py0'-/ ⹘$)4i5%C-gi[afv5m2D|!"{ Ԫ}:kLN$'`xRuQq`S)pbȕTi1|KM Tn]BDQrC.o1"6 pҔsD Ji}ݰ5v1l5Mr!XK XЕdiPPKL-X\ W1WU3KR'eS"O%b(t´`f9٣{w =pVĄct)4W.kONF; $M؄=Uԋa‚.]#@6ȁ'3l` v9$@aarEwsP/ sNj\8.apB؋yMuoLQ?)H yjj[Ʋ(:~2ú?duUӫ@ 6)Rʥ+(EgYaw訲Pz$!Sv"Γ+: 'ԦN*/IR"k ymb ƫ 2CC `JFfmxD5KlDu @9e#i[,&"w9vcV: #/KbMEhj(`r#PGIq3*"%JovwN:8l/!]zmh1(PIL%CLFdC:#^U=ip׉b HMQ X‭|~'Vdkw|Ng(s^C\}qWdi^JM]ddΞQeEͮ';Y;&oN`)'O\_ӌKɾփ}= DZ zV$QG8Y{%:7 u8`^]eՆx8͢LS$ COŐS$#5bm}OmKx>QF9N$J'չ(^`#E!ptZM>y*`kq,Ի2l|bK&dz%acپ-ck!6eIxNrO av}VnA}%X`z~j9=_/Ox^wfSUh*zcN9;OO e![kf#Uo4c2u\.~ٖ2jߴՌZk0J1{)KӅ-u}X r*_ܓ$FIvڄ)p){ w[\pqQn*kNt]ad4+3t'deMGiOk}js2J4Y] =] `+[?vҒFrȒ(Dz0;cX c\<&tذ}"hDy(B򥇓f/S%Zxys ;U=D*e7^5sj g}h%DH$7>\rSdgItjĪBjh+I)Y=_mg|.c\$Cj$wByn& 􋀯0Bj LI۽N CC(u" {!W;R}r\RjRxd|o-=jFhAK@T*{Izmz%Uo3h.%ԫWرg6x5=Y{2<;J 2_wlnFOTV4=WO V 6Jm,4x( \榠G(8ۅ]+BXw+8nD uAMgQdqBf?%2_!P1<'ۋֳ߻D@ !RΆb>ݳ2y8+b]nF rS-D."p&8 D e5B7 s1e[aK#I~a;Q@o#(/J}~L뽚UQ~Ǣ+*0}Wl|pK㐦v dIϸD 5ߵQ猂QIn/c3|WMPI fF{g(>% /Œ-;cI Lw,jjp=Z' a<bI^'W]Y*á|hq sLyz 8|"*Clb!M , VR j9ruW>vH*ѳp Y#%GrD5N/bc8 _u|=+5AP&JEzX>˜t!↨+:Oh&r检?РD W>]d!hʀ/gZn|$ l<{0`ͯ$ riF A5b1bo&PcA bK&vjji-Ϗ f?dRٞ#"F=k8ȁ#搖X0l!vHGRFafD9@0H=ǿ&\J(l<n`ƸF,yDo 02"`vM$g'W ;H< 6=Ff!d2ٰ'}I柊ɷ•THPRK8zbJgbd@'%#K e,6؂2.0`uu!j]O d?yΣ&>NC7Y* .4_۵׾>`TA\O雱,ʄup!/#@`G7/= i$¢~J#ײg 'OIҪz?JgPAzHEC&P|IQQ1/AEd AQeb`;U0QU g/S2($\Uq!w#VVz !(D LJJVO:MH=Sj<}]b_\XCR?4Nbv6ѬPX&EZ?&: ,L 0ذ'0`:N/($)4U#/y5_ä8U =Iۓ D1t "@$H pYEl3r5&>!nſVr68l)đf-Bu95V-"1Dʇ0QKLU ۡKKB3JcRq#ԨhL"9J>=OFM}/pK'z:U5`f5тm8}XFjz Re3ۢ_9 bV&dTÜ|vF jEzXy`m ҇&3[xGGɠIh~3|8(GlKm2}TCQm?U @'짊) fŖhMan걼eЕR1c@'xg,H=\"#>s`lC12G9J Bl ,xH&HJU6Z2m@>Ɉ [uLFDZ.D d"AMՒm8 'zHTE |@dpPpz 'ެχh35' 2|CA*ɢk1j\ߠ{ěL3AAEo.l(V^5f=yļ"ћQA 4̩,2\ܢ.AJfl <ˑ:de|F8 <+u 3ӌIQ,D-v .2"NeM- 5f htV4@>\ٝ4ZBYUG7+ !-; @JF>Fh؂.*I` B"bo}]yVbж3U 90BD1_}d |?/+fmc"O10_ӡh*. oF u0>aR90c*NZ=0ፁb_u FN3_ݩ &hP>d9}*U _TX# wR/—co)d  ?Iˡ{~O\; \I+П^hb#Q!|1<ȴ"T*^5ыSZ5 o|#S4Xe12]-=Ú"\kõQ&2Kb)yf̺>M2iS@!jYBFZYQ:CNIN8r~.J۞=^H@.;ā>{ I #f"E(-@gPxjې@+_g:lx[̙I&Ar2y8UE0`#˥y/ K8Q5o0N_X$yӯed5LRHfWH|%nxKs1c㗁q ዾɘTECB@U{*_9 ,U+ =4(XOz6p^Yz6L&[;ߐ/0(@ >1MG.V~b~E+Q26I,Q%$DHiq4{N'qb:ltԥC]jy evc =UIX*=Ӏ)KT*<aI7p']J 0xwNb4Lvln)1XE\Ǻ)t3|iP6ѕfDsdxm'O xca4Xiަk=j{:'؆MO N*2duʒ -=l1f6: @D |_cM9 π2<] \b6l>X|(!;4FOW"l-)MkmX>-%'wj t G|ɭ_}Iq)dpr/ jC?}Ȭ{fW穕Z 9ي DPt]4Qt$c|"7FpOM;t-»͖m@5chV̦]M+u Ԭ &LVD@HXtkt 0tl WK]+@"DB CPaG14;! Ɛ/XXb NbT4`!C3 0B @J?>C >Kㄼ<+8KGXuCƺ}Z ru\;@-g3Ɇg:SspWră5"QR?WO, 㡅{EZf `|LEe\lxwcqjW2ۡzX7ֹFEhYUQEsŦ>0HZ { \7 @WMŒ yz`Y\7['[]E6u;Rϛ}ўۖG;{N/,<>HrӆaM E䂨AKT '*UjB( (t$QQÃA"$ /D=I;qꂱ)ց[l V$M"&:kj h^΋ HKEY\CAh(®WPF'Y&r` fб &#r1cgg(<}d`ɜ(M JVMPdHO-*apVПt$Q aF"In Z|+C|!A= "\(P BbPJgHg ̈C E$0L !^qXkԊm1;O€ET462kT_Sfe#0K]gEtOEݫ!$] sD ce;8Kf']f72)(h2$'C mWHdL$%1U82.ɿ4-)1(Y}V50A (xgrvj릯?:Y#:|*]^4p !OA b'g &G)'/GG>upi(tQFj0"\t}bf1J,/jE_B f%6̈́JR백|"JXK9֥K 3MV0>@c?:PǥLtdچ#V!Ñ s6ӧپ_C`YbVa;R:ΦA`롍8[ƯX&H9j \J@Gb4Ɲ DbN@iLHKWWC "]!ZeqŌĪE@غb _w Q1HJm*ڈ4*ZYbAi!uފ gMH[č. ;. !@B3GV[͗bP`_Dip>*؋qEeFmRj=팄6zQ0î.fE"4ee +Ll#bwj3cbpܦ0 DTahomaKakupoptaiT0ܖ 0ܖ"ii i LPza ( TahomaRegularVersion 3.05 TahomaBSGP4CU3Ifd<+T=:9g@-Z\Zọ2 J4쏠%X|P8+>9I u`Tn98ɱj(m:(a)O+5 FXF&P h'7Lh\nO)bhdO}S xcfB3!:!)bDDSzuNCy-Z ŀAEsZPHx1Vj hczGJGL؂51eLxhx+Bѝ蝄 WhmrB9ը<#8^LITrksj*D>(ZFDuS KU9]Z9v ² D'D D*s%򃓜ĕP 7)hWoH> [j#sglLNڡ,h@k^ni<8šp LގJ o H*?BErY 5PQ-,T驢WѹJTK %V7xCwkq!Jי.XVJrJT}IRXUwfKPTJ4]n11yF#Q5*#gj,My͝ވ[\u^6ԗsY-v;ȴ|=W@b_8>8% 4V/U:<ЕeF +zlگ^3?ͥlFZ+#u@ZRKnM)JZ&(zm۔ҟT JtJQ _SQ !EhU"#wk àLWCld mٰ{r vlo( 9y# [Ø^ 3w|"4 --CJ-y*zfl:|g%p] a =P_׍`L" yi*D4E q`s{07x/p&<$A !BȥyۅðL[#ZaYfPQ-ޅl?Ď17uJ҉oRB0Yi;(ʋ W8E31* #9OEC,/k&9.UZhCNu#R#%G6b*ec GFu ޒ 7'81wv]KJcOX%U &6)FT# xS\pΈ Y(*ᩈ>~fj> Av*3rcΎM:qa EX5Z _ 9ܕu !9C|\$B;=uA\+&.q)$1m3zvD;R3E`6:h觇ZJ[5@E?TeN=pXg K,r.ȥ2qZyk⥨fFI`ᲆ ʹgͬ5AuO$t6eRH½={)kXN@c ]BuOKoqMcζmcK`ixI Mu&\^h!ctXx;><|Cz!|A? Nr2)>xWs3!`bJV5EjV=٬ښa} Wƿ!%"R{iqx4$&< ٩] QYEv4!n'hCe5#&~H8DmXY$ZGd(u7ӟ4zO8/)4]QDŊ_=^2}n >0H7$bv:߬y,&=…v3zUEd fCm|q>/K$%_/ۮHĎhpē!Ebs LRO{#}?!@9|#,4b;MdUlNh ɬGP=0s#QkfPiO PC I6.=tKi|'Q> (WKb5*'#BX@r کTwep>&3Ϙ3(T@zPb1G}lm10ZߔBgWji:(g: tO˕ljXy\4HliT9y@+'`}UmEẻe .a X(2*(B)[):ny?)-"t)4 v}߁AkeG#^B"Qn~G%pkMgQެ$ *AXK[l+.Co QV"Pr83?)FBsg6MiX9KȻjv>]+tc1A4l{z5Pt]}{,8+Ѣ(s@xZ/|`g6_ $-KjV&fi;*icnb]!ۖqEKU2ze;υpWü-:ČPD1AX#Z̈́{.N*Z}$Do"6 {cQkdd a^Ф di@kckhYKk2S$ڦ"ojm&y |O 9<n<qzlR⦲|CWa?ZΎiHVޛRv3 >K#m٠GOp8oB1ƘFryHU>D1q13]DAѥl<Ɫ>x*8EW?O=N#3g'柕ctW˟G9&-Q9 Gy8~o{teE,EDIRAN" nVЉČ2r7BN8 c(# = 3 Y7< ?As;a pl@ nE}C$Ld$ D%Q$O8p9g2q(@p}09~v isEȦw8f !! HCR\Rr7ds:/  Pw!\uעJ.ͿD#"5AӁHouÒp˅4HhJQzt1OV"aQ uGL Ptc )H#(:QyZ-͢F+28+]BIN (Q`#GF¾$5 tZZ@u7?3eDz8A㷸؟+OHhW%X{38يGWN2^ԏCZ¤hW.5v3 5 ( vf")3)V`̺4FP4  TyamVEhr޹#1yP3Vf(vL{Ko"K2G?&+(*M+T 7FNa"gUid~!B@,)@)ehd*4ȕq8c[#3/q`yR$uH$G48i8`!(J}/ CD ~(s yj5ca"DǢ>N =ؓh^ߙ4dB' z(TX3!yVZy߾ǚ8FF&qC%· Gy![.{pq:>xp:t'kP̦.BƘMGa(/,L$/#\PW7Si(oB|g GS:qF sg:23 ga%A)UtV6w>GŪLjIew`0G_7J\0*TCQ]P+?Q~<߄(v"vElz#;Ī`IObXѝ$qjܺ('y0Q8?9;OW\\r N^krXX=bĊ'_IrB~MTsQHzl @G+89 9L<"KHJ>yBF/laM{vtT[UA&1z:?:M[AQ!o[a,A!x[I$~QHۥlWkYeor?K߷J)kjF?bRwAʸ<z% فp;coo-M2 ,.NْyJC;@GC_zۼ;׃QzhT5 *If6њZ|"#,7 oytMlsJ@qg#W漤åUy<3>AmMy<(K22u  Ui<x l9ŪϳW%TIEt`H1kero!e-g] m :O}HəUv@C \êY8d5$`Bڭy4,",vC~U E§9T놊W߅}S+7 YM *R駩'LBVFDGgi"Wi" *,-=|`qVGQ%ޗ6l)ǑT nb;L,ըRXAʽJe>Pu I*ƱY0*в]yN$PKK.Ri+0 (a)" g?Fmo;#43!5%ᆱzY3 W&\qC.(5[!hf;Dksrxj!amCqtrx\%w柉0GiN7#p`>mVxJ&@S,~XB5Vջa?Tdek8X^^Ѷ:=}v?P N ˁ3Q:SĒ3Ʃ_U848ףPR҃./6-[T2 Ũ,넝D%gn\%rRGmњͮyuLѸ4/k ?~1$AX<ۣTu("I} hߏϯ6gҹB_̕(hKDV"^[{A\V&s9FI98-pN7]lmmAEŃ>hl(xJ8͛sQALID-Z|qc2wkC'Y7^p] Q`Y= `x$ Khr@"dudwTEQ, ԕԜsaSE8'Չb`h'=|/m@"ZJߎ+KNj)t&K(]1Q@+.Ʒۑ}:"gC GiOp<+wPv%>qhH.Q4"Ιeye#Ճ]c|ҷ{n+$-/2RG5]GdڱZ[bQy<1B{[C^u$Q5ZGk{{D:fYٞM),!z @}wp1;FfO)c֓;hȬ`1u ",vtW}VEA\ *ց-C :λc?Ypu^.L|v޾ui?(5JXLC~ wfM8$)Wpp*<)@ȎIu!E33"Mk#OkE!zJ|\HAMƉSEVP`upMbEVaB\>6ObMm6yM'A>{I<K.K%'bRg`(Ysrb66N 0ݳܢxNZ^T\A0Ѳ_Wo#SV 2BY[Ok?;Dĕ%hE>XTNP$"# -ˢ)iPPa0Ȃ`o ʢ|ވo J,T`l`]Y[`Z䕴!.x %VTI,4IpZ;778-&]0` 5L@ǯ PbMY R~Fc2 סjx IZԭF^xwƏ %"+|dFZ Wxr% BTCFR%,(2g.|(S۰*wwZL#+-4Y^&"fD-f-h{6 xkָE֡F8bM[jm&pg 1?PuGm͊".EXфҩgs5C+o3l܍}b[Ov-! k=. k6~̖rRZ?r0|2Xal@u)lu)?$v H*H M 5MP$bp;H6vn.U6t;t0*+FVcEp3JєYh&LOLTsAB\^D+=5T#Cei FM ~;{~#J mKPaf 7k4-_ўV{#K!]-'7`Qg $@ s9=$&ӆ!`HCv6x)CaP~ꀫ}>XE5 #TIF1k;0Q2"EMa5;EdBHw  &%r7Y#n %fTȰjHl9Ho(J?QGEO\3%u A1Kll(o:\0]TOTc>R= v:(=hhFvO$i(`|0Jlzt&)˂꩕#@)BW:/h `$%e@[/嶺@K O:+NCBCC&.7P;<~F݃|,|OٸszbŞh'x*OT :H'#٥_5!s,& G}G;D`HUV!v(Lք9#vХHE 2  wh\m8J*X).2vZ$Ɋs>346ЁhYt|!s=u fߕ &suԢ\:\d*"l oO }өtNM^gOzFn ތTa#汑"s3&! UCuPB 5Ɏ !B~x3E/Tad8.uRkETE Q=h',ԓx haHpܳp`\RKqjovgS_д0/FȥgP% NDto*¤tUtx0m[8e7dODJu\͓j0^rFw^Bu,!zFդ@s\%(#um5HT<6/$o r895W'Y$2|t$]$rpcœwvRSNɢvYyCFw,66fslJHBh7܁`O#bǜX>EFg:"fY]+Tgf'8ƶ-Dj_:a44C$e+WD - ˵m~a >ΐ?8Ӣc̬( ֢`\=H` `I锃_1'lĠ4ʺˠ}O ͵Đ{Ne PQlQDĊ6ZQ(А}M Cfv k9ERZK{#D@nv-}%() FH`fOt+ +?SlnI¯-۸/dp?:[/@ba7잕?$O yXU>~WQT0DI0j +22LzTkOrde93hE,e0E7)8`1qaʓ)av#g4g<كOh+1$LQ{@eWKpxc|X9]=caA(2qj jAj+7W ϛr)[GTӑR7s"d& R1l `4WNI_XqA'4"h)On}|LJ-EHt&D@!y+P'B.J2bK.w^R򼴄f2EuL$[zָ[(.U5aHpWd3% !<8/aS+3 9Sgt%K0fAvh"`z1"ؚcw FAY515Y"]&`Bgϐ?و?Ԇ< +>xɖM ߞ_եyGcSW/Ӟ d gL"F| J8& A0@;IMDPnN+:1-$@X:昊 06䐀 amm2*mPSfNHr-ƹ?"# }~sHm!sV!Ne4`~/*V+Geiui5Xa 9No;v+>Bb&bcwϻ+` O Yh~ ҌiZpa`0"~)c]|FB@vvPH随"",,SI/ѐ~Eri1]I*HX{][]I΀aaKEKI=ALh):\Գ|l9Mv]GԂ0Ƥrk\I+ؔJ/?e@L?7Ny&`/΀6 H0%7"7 ֔Nt@ 12?B>LD7Qֲ&cގ&icP1 qp3c&xIPP^^3ć8j)2b$jQ>@"qIg'A3:Ee7?eEܱ iaS[[uYZƒZ,ʂyiF\-l:6tK߻YgNP${#rΌmZajH珍CkU3[ W XSc^T,DէiґF%] U× ÅIg}N:IЭ z+7rJGȁݬLg1,}#pƗ@'8R~gO?px?$N7"o\ʹXbV4 uϱZ0<$2,27}Y;01wf9XEEeRյv#'Ѥ5H&OlQ2" dxd[8Q R_Ŕ^8Tyqs"wqym<Rv)vUQ$e33UI tl6i+־ۃ3oOv_&J'Y2|^n 8^3Y${Fsl['ֽ8fRGQ1kR[ZGJ!5f'}ƛQ0l0D]x5w#{h9\d6Au}Rm:ڜ EHfIˍJs6OE4qc@<>SÀKGfQ)q=<AIIqVج̜^#P Wȓoq$Ӳ#a`C1q>>" aW x|z2N!@"5K2ږӃ%|:8r> :\ XK `@ /Q` ebƠL/`ͬ 1z}ȀGʦ,\,+Z.3}-}ZdDޡx^JSXd$sEu2O&K0_JKX2iYmM^S, ?(vq<@hM`hV1Ep=D ha&IzYELP"z@tχH3y?.TbS89NUp@MӚkwEV_9)*(7)L RR".1 pЅ|*]Ak.W2镠u\ڢ؂ٓܗseP6)S`$"I YV|:O佦@,L#:!jS9)mw97ԡGW`Mlr'ZQ-Z(X Hht$d7 *J9'WΒQwfpū\28O]$ćTJi䀘Yc$b<7a'IDګ,Pu~(Gn-C;wlP&w!'*XY&Td͐^ثoUv]w D%gB/75Mgе DCp9n='q]|i "8ZX\WX4Of ` 3)/Ē(Wa϶/q^=x<6(+AxHRwhIeWn'mbҰ8 \< H$ \u}!^j*Vuy%I5If*whCΉt=Lrk@n-Z@<qb,>( NOiz$0l i RXMo]4R5v+ fɠ8‚a\YW+ m4L7ܢC BB?٦yklj]bʺ5$?s?䜢k[9΍ CF-\BhOi$rAVˊ,fJM(媶ALT"-R{N97b4t߁M0b`Gd4@hle(IF U2J%V8!b鷭K6!ǀI`-(@``vKa}9N$=Tœp\7UbRpѕ2pUm@1Ǹ{A*2B/Q_gKVj`%kT݋[d k˪|y&OpnL00LG9ڹQd46DDJ -DVLFU{\1OԦx@G*%ѯ _=nT2V* d7wMm( :!W fa5| -g$GpTxXDHC %^-6̛j`?>$M{^>ՒӀcH JopUt`xTjbHݒw@Ea%9]faF YxLkAsxÁ$ᗽplIJ!ͧ"f : i6(5%z"ea{N" ו+mH:{ ?' ְg63?l VQKƴ-"rCDy#Apt%Vn}Cf[KY5ȢIpg1k#W V]DG3]lQ a1)|Ye_xi [5»=Cd k{Q׳ |EɀlO LN gE520Q1KX%_ l;3}uYqL'7kx-dO5(e{0Pu ;@p!@uhHFa{`G"AkJC3,(dFw}e>?"L}M(ؿiH{Pj6-Ȝ5UT시w&JQ4U$d;w}호yl^D]*qHqv94E| ^D CD]@EZ=ߘqÍI`kqYdJppi '|v$I}љ]c!g rS2Nym=u`€baN2so[[o ACQm*'_{3c )g Zh&a=s WdW\J*Bc_ܨ>H tpR(RS0{- rQ ep%PQ2Fa |EhG5Z yl(# 2NRޞRtWF=2!z ;]Q1j`bdgSdP-8$ 8N nKe7N%1RWAQzDiHT8?Y[(%P ѹzX998Y{@*@E``V 'E. `8:TĴl bMtv=J aSidyA:ܪa?A|j x-M`~.U$b3fn $q"P҈ut(HK"4r мRTa !h NoɀQW&ѷQn9ckb6zr hh*$M bӨ2Oĭb+$R0G(by)|qd*-JగBI9m V)rO[5 o-MBEV˫39MSl2Q{ϯcYJlnZ>h}Uz'R@3p=WMi sv/#vmE.#57 000r^qټ#`](t'a!QsG-aa V؇B??,XjHg,OgA%~$nIT]УweQ#D4GEV {C$ґ6(BWhњB*1Y; Ee'pG<\/;44+rYM0cU $FA\5'1Hd^E621~IHK_FA<_C>Ve(F6klq_, .,-vg*4]- V"͂KJتZ8HzBC gi$a0SHQ)˸'h Ї?E‹ Ŀ⯌ A092L߃wGBq `}/ `a$5K:Gv~!`uXNfz[/c:%KtCh^@5o$$4 AaDUo @HaE-hԨ]Yp8dKxX8F#B:*`p_Wk#iQA(FkCbrÝy@x"X] tJP@sEkAlZ@J0Rc!GNS m wFV(Ņ'{X 61BkSFQ:3VXV;D6e?mA.pp[&EѢ#y*vN6AF( eR.P"y"ʝyTG²Bh{3e''iZB_Mg[aq6q#=Tӂm@p/AXfPiB_ACDĺCʣZv,ާ@zg(!c$?DE2X6 ]+MMx2 㛃T_)*=y5?XRMj[cؓ>SOxtD}Am#U}OiǁXnDv--JȻuLaD߈Ʋ2D^DcJݿ逜ߌxo(a܂|WF"0q),()i1w 1wDRDYx1 ^"J !rDt>|"~ޭ`և8pDe+ ΂& $5FXNh=*!_E˞4M[ȇ.{Uٮ%\Ли;\q!() ssTN3)JvsDwF2e ud0Fh0%}l!zxLZZiK$c@DA +cc`BEZ᎕1Nsa ńr4n*,uȾ+;pSiLa*%K2E1+`]3"\r̡["ƃ24@vxMJ)k/h\k%}Bu !6]រ&2F l5 M457įD`tjHLJE;.=7=g)$!()h)s%T!VZ;^0yj%̓$$J]̒3G!fHt=ҍO[x7#d"81ABTɏB=IkopY<|I)Cb1o dowhd1}%K1;>LIhP t`P@fn/Ko}X0sX4?9w9Sg6Jy'%Tم2d>:bDONl0|Qs9+1uhqDD lA"8rUΟ1}zr81'bJ@Rh)C zp)#H'L 템s85^n,JK1pܨǹh MBJ#r0*P# 4b&w!g 4ua<܂[#5QIVűA`(_ FhȔl ESLз;JUsہQ乼!.Z 8`ka+,d@w*"&m]10d 9AO-4?`bYR:"6i$֙(U3(JnP=_8;EPRP9?M>@xYˠhρFh›A8NTw!@av}+"czwluȹXsb3 b c)SUmJF|@b @jZrcTvds&X1L 'H ch8U<ɦȗ|>"?,I5` Ӈ,L֗"H% ȢjȌ˚w lL!a,7 :r+¼̇t\1u$5:Cժ<&( _2~\gq=3 VseW ys3Q#(_pE(߲2U VaV`iR6=9"d|ORP#nn VAjךF'KCscr7Є59s5unE†MTۇj73%T ?LֽUmf(*+qA&nS,[~^D!s34Cxk-z)̯1m|Hi"(ӆS<Szz%?;ΊQr|qiG$M@'GV5`N%{P݆K3Hi`|HoBJe =$98(|JyXI< qv7F%#F~0?W>9M%X2(PPgvVöZ?  W5fM-qtR Q ؐb#33M$Y@ _G KT#Ի/.2]J8@l 5R!gg |$V `5` y7'd3G2`Qak^[$* "(R$-KDk?} b Oi9e༙ D$ܩ<b(*ɵ贲?F-=Ϧ6ޯkp]FjvCWY+i4I4 5oe{y8+Pt7ڬjv'p us(gTl2Z9P^WW%AzC2762|`WCÎ"HԺ5U[TFuB1!rlQ mۏ)_*dGDʎֵOyV y&Bc%( twyf2VLsI0K= ucF&HQ9a C)erE|~0n"EEg :w˓T1`\U9KDjgDz38l!52!"if+H**2*Lr 2_1Xu 5J3_DիE[]Ĺ bwK>OB0igjw Gh}UVIɟfw#vOWc|R%$АXvSи#I8ec(r3~_DAQ\s^+[[H)k :bi'B! FpߦMsœѪ'f!p 'ʯm*U&KvM(ͯhLXq_tʨP,Ir4n_FY2!,ű؇Β:I!_/4JK_-! ,a n'\eGGݞAV f fҸ[FZDP8ZIO ~vu c%I*D"o'(_H8P?V$WUl&ZF?&Q%ML[<ʺ ]sK^^@ߝ̧f >gb]qQvQ&({FtTHhTt^>25h檖c`Go!V-}q<屛qRH0&H+s"$0C - sK\h"Gf^ 'WVE1X'|M;tD{I7(hrIgcqdzۼ6T e"aJx:.)96} D=xppT6"ĩ6w !:X>5)*z8gʴ̍*"H_nd5q`sCiEzyhH`+z@tG!l`/ÒJޫj!4 Cp2J'⁶ Z^F2&mv6Ecv!)W}a!ybhdQ^h7H%ôz[#pavyoq%I:r! [wVƾ@ٯd IM6F1pf lᡫ1pq8醈1e 4ӵdAߣ5o*zd`ж_T l6r΄;{EPo3kNn0j2 n!Jef+#Lg]t饯\)pJ+Xf;Bޑh>R#*UWcn=3*Y#,Kn(NY7)Gu|p8h.fOqɔFƃbf~3dܻ'I6v"Exڿ|QM"e֧!R u]=,C`qB!)3Ln(Ԍ$Ѩs PNTB2xlhJ!4q$"`hL勳OT۸i A{-e H ȁDQit#6iD=LR3.a>W:zY`QE)8') ;_l\c3L#>' 4[X*T@@`܍~snkۧnLPKVDyiK6qW5HGW5,qP!p2$m9bFt-p0@OHܶMo+OMOЎl _F¤{V|Hh.G7*Z4\ғ +AR\/8BBPpbp9FXmֲJ=4BQ^~;l{b=yLlة9q6^RI~_}ap1%%Ч|ac>H<+cl0"T/E:JѡVO/O9z:ڍbˬ2=݄_XwϹ4' X s-29B䦄)uZ~En#Gq4\HpF:)DѕvsLfA7qؐK -*0v>CY *dX!e2#ΆE=*BUġÖUQAY{: !|QRPI܊q-h\l j`\- nMhj2~Kb B~"G]b Χ*QN'vvc,}3 ND9rw|̱1gLŘ*6XcbyyArCDLCMS\j/7yu7U(F^]N{3lewXȻ@6A8l2Zq@3<+^#\)vo.P:<>6Fh,Y /Q!F[м(buMW"|v Ƒ36(d4҈=+O{0"鬿KV_z `"'`41qo$,7F-ƶPRy!^ `2軵!8XXWW LPza ( ld>Tahoma BoldVersion 3.05Tahoma BoldBSGP>Og/x yWPxU֮;GCs(<vYTԗ4IϨۗPu錎߈aT_І+˲ª ^8i#B@txt<kuJL`)PfU%UMÈjX?h7(5!!g<`@;>tĜTy>Ć{bpDڣW'eC¨so݅7 gG/`Ů0 *j_7x% OI_lZ\_ʨ{rG %0Mߔ~Ǡ4D;Dxs-$[HO{Fybu_0+da/)Uoݠ@.蚶3zQ5 fVnUeo*H(;)/ռI 84^kbW( (_)O4,9EhAJ|]ј$)y)<>ZUmhxM@Rnuh1 ?Q/UV5i$k.̍{`7u&?,6Rz06:A<݄]Zf)."p?#YFlcuL3*E 0Pf*ٍ=WSo%!ٸ+<AiaG}+ ;5DhY39n#p9S@R2l,l7 K,yJ-1<H yDdKj"Dl@""K 14 4>|wT57IqDl[;T̀I8R(UV4hv\V`芧Z]}X#~i"IO6[XI+>w [z3[# ٠)W }R9*hƖeKK,́@ V{&|u׮2&d$CX"d^_Q#zb?_um"C*};|(x]~ljpFrT2,9hʱ:bYARɇW"¦lszQ ;n )d(Z#Wq?TCzda s91W`H?k <19P EP$eDI (0tUNCk-#fUoMgUEXT e/(]t|fڠ i.rCꊨpDv CJwx&Z9#}FpVR#+F q#2%0WnC# S K ٓW &9 -vbMt 9H0|Z%'zMdžLD_?H ;;I3xekQY?^Χ}RA5!f.hL[Hs9{:=^-_2J#;1 Y:_P!#WFH.p *]{:h(,NnR㞏3ba'me Ǩ(DVpC5iU?5꫎Pl,2 !ՍpH= xA*f'S$KZ@l|O$V{|Bt9fP+ȐnJf%)T'ziQ @jdE 㪝mW*D !`y'>n97&~TS9+\"?6{ <։ 22. p]q?94)#qYuk*ma#.ŚNpLR"4 vBDxsp,P6$7X"湟P;qiТ]OvU Hu.BLN+[bT?%1w0fҭcpnOֻIԃzvY"Iz6L +RU V격8:N.4y>h|,y%3n%А&eR$4x6OyLA¸T`sО"L. CN:$ M bj*]tyL _\BEnnu6r^wdGia6&5`2Z&V+܄C 65Vɨ>]{>zA$ z%q~4￉)}Nl_ ρQѲ3E쿚bfXu(CR}fY \n<̄B|wđO+=BlhZdYszv!#]?N>+r0ӈPqÑ#* YݺI;GP̋h DWp[j5Au ;;[;.wgjOv\, aD-MAF@Eonvٱ]uE)Kf+XA`ٓ꿯.aACѱDƍlK@\[ ؋C 7Jb1ia&RNS:-(d+Hd+Hx pߺ,\&t Hg̟vG dI3dƺ|+0RMD`"7ZOڤ?TPacD3X8AO SR৿#mDX9@qzlO 4F1>m?xR%7ݥgŏ2;~cєk< 6Q³, XF7y ]<3U)f%54߹éAfW%ZcIpt>'2=#titƅ#z"/"}H頊~ek$0\:7a`2inyQ"3 NC$2:g<4;@wMcaZ1 IrDh@.;AoӹvوZ+5E`HHWzP~D>ȓ$25Jm}*lvH.v /9g kݡ浆6NC1j";L4/ wehF2,:z"C `xft*d?+.F2]AD"؃[c+ R23.jDi9RᑅmR1iU' 74Bi+%'] w)\I.+E۟"_pڗevG3p x?0v E}~'\83B@l෇.XZ P'p1`B'3?l?y&3I~CJ?p= )j!Kܹxl-{߿5Q Bj!4$J{HjL^7O|L2֒WB6Iq؃ Zr5@蝷| ms ^ sxxst{u/k&d]f}2mMlUP4U*@bIjPSM!9'{#z(B@Ž(H# $ #QIYIМ!gԍb&$$X~(d.tfD&99HS=ɨMMx :ïua P(6aI+Ĥ/a( vN#'!T xOc9Wy֒LQ'2:7ǣ2rE*o^cVQhh j1 z1~U y!|iG Q<q.#q<"N R!G&7Fբ +h)).w73 [)KSH6gV6t!:AmcrKZ萏7L_x쁱(I6ɥ-- y_ki- NpFUОipWI+K9Y* N+=8: bW9B6q[Y~W#J5ߎv %BSTp(b@'u/Q$с$\kS[^Z ise~_j{2Sʼ泫-doHb>BGNOk?~CLkr)jA)&=K4M6nCM>\誕0-y'ţ$`% VA\8Pdz>w X2? I/I@h63@uA |&Xx"5°)I)JJrk K<JՎXerZ7L;DfBe2Y$.q3s Od߫vg~*F&J7AL8X1"uTwǙs:{lHnCAQD ݶe ?vәAHtȌrp( cP$Iyv5K薌w=NUqATV Há}φ7Ź7ɭ2,Q,2.{DVUt C%kЬ}-B˔R8Ng t3S|2ZU )$;BDW$NF9,ZD0a@lAM A|e PoyGYZo[yUȘ"C\{;j(,g8=ƿA*LMgt9; ӣ26Vh]o>.wia> +F`tBOҝ4c tdAСw^ A2ItNIGw-C*4F=?St' /]qpMs&;$ºjRi|p5$Zt5' caO!)FA=E4@|Y` QYumihOKg%4MMbhD(8f#O=\ꖄvД'~fJ?9gdLPZѥxRU0 AL"IG%#^Q8f9at @xxF&CnmW.Uz&s -a0ODe|*B $,'X-\S($kRJmYp  ]@tiuUތ`p60 *:}J0>id[*ۥH&XN.XG˭,\!qX0grd .>l2k-l`qLW)us޲4wBί\٨7י:5 ˍ9WØ ?ƂQ,Ȣհ ^@9+[ &Q~pЀ$f,WgG&C鞗qث{zh}`waVX=wg1+)P$P6)|kv?dPZso`~xz54Gr-D6:]]sBMX҈,> hb!3&(S_c X* e R(nD2~?`44@l*Rd@o&M(P*O.'1qbqE:eqn3yާ̒nO}o yO"gkp9o[Fy-ns1ðz#Mޟ\]Y+.rEa^ÌBG!̣9Nao"PAO6aȓvoQMpRh0wayȱX' I/nr}V Gx)a@ڭNH!&.]-/\ *NsN]uPݢu|^#W֯B7gt t4A!q_aw4:xi W t ,ӈ?r'#ILr x+B8#41yd,z͚?9놇DYom1-k$[/?Uh A`R瞩|ρS9`i;0Peg{Q<4jNOѦɘE6w`14SҹSjz7n5HyFȵl|.`vß^!?'Cw4ܔ%X  Xd9O WX/ql b*iKg;=Փ3AVe(Kkl6Λ쓑ǷPL;΅Huϑs_kr0;y?:[Q~QQ1yԥ-$k 2k|nId;/Gŝ=X S@7럋KKl`+= ' [#\/f'/ezm'^!{F]ӧx\dx[-to̺f@}|ACOnGR''q_5T0Q;x&]yb7'"#sV4zɤhۦupA y$Fikձ0 hP rO~2 "4wVW#8r@І?7 WU/l 點8+M'-7h1ؠ/ ;e+%s\>8;Uzݾ]Cy_@(ґźGӒ5.* Bx  HK޴*yˆ˛K ?oH.@`Y8g;cZ zgK;Z-Stn -m+`$IS2U Uշ,~B-\\6ۯJ/čف)5)RePI"MRkl.|yT:N6D6: 1Y-Kjx${<OP+B2p s)44]vj>agoJxEKtEG)^sy!O>P_ K6h֐CH!oWѕa,ₙ-ꂳPRD%\魩BiEˬB1-fS)nf2u~lMj.#loqvS. ?7/ÐP'l\` bܘ,tHjiҼg%<+~4F2!WU6@Ń,@KqǬ` (0ӸTA\}DoJh㧍 F* tWb+e5jx=ɕIs f;g r/.\)ƨֈ r9_GLUY5Yf0 )}N>]D>8I|TH)iJj&_M:wl-(ɘUQY8,?pZ_)#; lJ\q0J7*bŎ,8^SX'!+r+ t'N_n[oލɭ|mEG;E5)=_"AЀomT]1XEE ^O J.E#)2@R}.nA϶Zgq@CYĨ/ 渒{kE ~@P@^)yv |N=qIHd)lxɑ `uj!)d~'G.LSI3?g)9Fw9͢'=`Lw}.2"4 ֎ I="!ogV,Gĭj/ tB6ϒQ^֮!YL6E5$,ՙ1:c6R lP<ʁgi"h7ml=r;O,$ ކw)τ-wFV}+ {?}+ŲK; N|_sx<B+ qБFV}r+dq-1LNZ pG(55C^FRc.-oB2n'_6ϵ#"qe/'> N7Z>16E!pv+k SRL&ܫQ3K:f8rp#D]ZK}uj  &*6{Jfw /agduȤ >tKPP[ 7R$>385ŦpaflcTlfN-TnЄx_K88n\ ߌu^XE¥Px \Vh@ѹF`OF-AnXPyʊz`KAا3aʎpT|>(\H*8>u.x{Q0byrRGԧrc(m\3`$"O>ەu" dl) KI1t1GWe!z A!tXI_)7Ө2Cx_(;I6+ђF+lNcv Ix}&lZ#?cP@NXGޗ޼PSAwjVLKNg@'Lvʷ~a0q' 2hSPۚ4‹?=`c<z7T&#> ~+LFsןAE^ɥհD^*WϞđİ1w-!/%Ŋm]6`y_$~2#eH̋$c<+9+Qf Zl*IW*3\ )zF8O<' Ȯw@! 5h$:Lvin1)L0iz)%`R"!r24R"|sSΓݓBQ@sЦ9$XBDQ gz\ 5 nYi.aXAAs 84 O <;UUd/\#cJ8 Q;#ZwޛMFJ\dZBjZ.8qgٓHtoǂ8cgC:-Q *BE(BuŸb;,W߸q o 7Bĉ G{U@gT (g8|P(ZOL_XCp6]?Be8 0Ka:#?u\O@E`ap4٨^_<:` t9IcI/B ct(д[C@mER')Z(^S*W犀q` L'88nm |')?\=(I 1L|O8zP~Ӫ46Oi5Ώ)R aUEqQf-_'k7H]h`jzgktfHt@)2wz;_d?X v"Jhs}"~D .0< $/,@q;bkܬJFNg*ܥ1eGs[Gz"v>SA1 bq£+Ԥ5llے<;ʲyJ%F"EIe?9#:Iyv0 m"#M1|QKƱ8A/h$Jf_s43 77fX];ƻhsh/85nvH3z4w uSiЭ#x8* *z!1ėcm# :#J:{޻!GS4MaL ¤.Q11̍T%2!m!ޖ7a-一?'O&G(݀X>s;-+ҨpecJaBe ^le8r;*sD4fT.:PkʤH T@"BC Ē xOHQST9Jd<ڑ75Q[zCE*Fv,( Rq}vx뉰HɘHŰ[(XnCfECᬉ>$Y{7{r.[^7J\} @o$bI3 g,beuaEP zۈca1~HO ca3]>ɾNuj8=:|9~E e vqnT?pFLkt5,z{㛱yA{03S cQ\Dt7MnCG]>clnF i@'+d݆*K%tj_b8.hؤ:P/4-*F\d {5-B>eú}nńü&!t2bu>;.Dhk a.MA tr}6ӧ0!CP:3Сljg09Rz}4ز#L@]eJB_@LPrHصVQB>70K(tVx2FH={l@[p:ͅ*´F< ?1ZKaJF![ 1(xZٌPcaL%w[̜Ί#<2{Dh89:|n&bGiDܬpDTjS *l T<%Ȱ͹%m1jnSe&"1i+BH5 a3=nDS0?y1vpH 2;y(p լsd^Ri餏i^I xޗhձP b Zi%]E(+h\< ;oK=fH_l#9f Yz:U)kX,!MB#l0]B%2o  y g?ep\/Ŕ/ 4b1 I7~7˄m>"% l p FIC脅2\'둎#Ze*s*)KNҕ!c& trq])mZԦ֖'¹*Z*aa[C`+00D܅(!>U8`?1*yAyXiy~\--'$¦17ϏKaxDq"6 sOA+F'-K=]KR HEýdkTfK+M6bm LP/uz dY1DxJ/Bi]-hPY9I}nזE;_β4Ւׇ eaG B>{d>q PFui%$$ǜ=sm#g !cu JU0@7@DS6{?o (Ne-Deʹ"ؽ _H )7iXgԈ9B.[C)遮Y0@gjI.L&jӁ h&;9˱ ax8#[-YqCLrǙ/p Jh¶t'{*$߬kkj=#Y!TbŢbZ)mwr݅*jr CNpXWf_FI2#Np+S'7gʀhK⪤56?f:J_<>&sO;N9>qsTgDHkٌ_X6^ B$` (쫠Y[)+k2PN8lC1$uh~"+<\@*'%!dH!Zq+YŽn8<1iv!% 1$i6^ݮh> Zά0w?nR2^.yuؒv_{V,DzRY[rO3I3܎RtX#?sEJhm/+$v@ ,#,(Ҝ͙9obkϛ8+ڬ*oi 7pf>q=~:*Ú]Js K26 nn0W=H(Ne 7-ln׊/ (Y%vP/QnT֛ ^HͰGޭD]12.!rk|9nqsN;:KϠqQX ڠgG}5 ܜt *>C"2xz/6- 32:)w4i'tSI|g fL#8o/&:ؠOMI8x$+ kn1 bسgZOu%R3|D|t$cXINz&;Rg,ll,I ã X2 ,MDiƊ#7G{x+N}/zg.Lބ\_ƪ2>P'[˜, j3dn$˙դ}Uz"r-&=~ `.40mGX Ҡ.vϏ#*SV%-Dq!K[BOS 'ӖՂs"Z(O&"Ќ|-A4'A;*p3D44IK K\ *b!e&=oJ\L^%S4B H5dk$o_`4gn@"NeDN]"V)'i?0q8Lqk""390ļ84I^V$CIHљ?ʘZG͇C kڌemjCREQ5[؋D("q",-nl.o v_@GwE&6!)8s,Ҩ YbvGٍ P,WE! h"{mJ['%4d8f`Pwnہ&Þe|3_Tiieъ% Z`57Yڳ -%Z<}SB-3N3EI֨|Hx`1A)堄Ѩ CR!P$!=Ćr6)s#6m)Or[g1D \*4*71 ,jɘZ qX\K!VM֩z\D>p.*HY"jN4zWTz锆KǎַiL1 E 7]MU8 <jx!#^!(N\|<=QpdE ٫k_qG 䄑L 2`_:dQ> pJe)O')x 3>D@H༢"]2w"8iɫ* BRVğMp`h`'A}r?_)6vr4iJ7חlwpSS?eď ͬrr@/ᦲDAr-!v6(?zM#Լ,xv*Ɍ?)+ y!!ǒdN)p^:t.}Os\oeD;PL=`>]KϤbeV}fe&4Q QŐ)@z YFK0=҄"ܨZE]4=C>xt"7 ́&I9놧k e<&txS]+Z!=g$ !)Ь$ ]. ʺgQW,-,"7rNW!'O8:n756h TkMC)a9S*ZZC+9(UT>4PD ]Is` ҉a PR{\l,(Hcf5K+B*Oh!nADhtc߉¨+{⾉N.bMyMA(0# |5PDB;@TD=t8n˷$< C֪L]GG@ @ jEخf*L`$KX·z@  !8WIͰxa>S oC|!-T LF pbwVE}iߡd|L9{kJє|؈'>z*R1#LLDhA)36ۨK+:)zXU 7E*Ƒt !D_ߦ>L8.r0.i4-t4}c7 =rY0FL^9˲*1Py+uX8hDkO_ `dUW,%.yn7>ApF?F}D`^lc4<5Vb8k:C!_QSS<9uR ݠnI cA& Yf!+O@g QF!(5Wn%-ת%7PC]Z4M6 v"g ͡$˂T|s#}9vSW{ւtifSwP|~VaQ "FcDt @>ۂĝ3A' (x~ nAb 9Ha/b栈aGeO9w"aZզ!g7EEDE6msت;sDHLv.NI\t":B)#AM=rIu;z}^e`<#53f N—VGHiA*n: :۴zpys9x;uv0OG8:sTB/1h)@x#"%E1Y R8fBQaLJ$,̃BqlR /;_N;ob۠3'ÝDԮ Cㅩ:ūV wʅd䗧HX(p1JfhI jeaM%P+{?/YB[*]`VHScrK"1XC K&L$_ӾSV?XղFP# 7twthhv9SrJc!4Ű p_6 CX ^OB, "t#N兇p%$ΖE@P>^x@q＜ z4MVV!!0j?hk5ㆅn-> wŠ s5~29L 2`+'obDMxb9 2 d p;aF`Nr#>=竂^+ @)65\ڴHWzU,k9k$@ؠS$1 / z\'}173I(;|- D1 % v7 )MBIŃHR| 5`b(d{+]A@#:I"OGzt$9=%3qzō+!ASiHfNX3>y vAlN/&inpC/d'E*ք$!RV2 AN6b1MYLK{cM{R-0>:F2g>Łiᷧ-' $Ï3G]'gJ$PLhS'fFNdyEvn!,CR9fH/(!5 |C)9V41/0DWingdingsupoptaiT0ܖ 0ܖ@DSymbolgsupoptaiT0ܖ 0ܖ A .  @n?" dd@  @@``    D_)  #9#!  5a5 555$     !"" 0AApf3PP3@TS?p@qAQʚ;6_v8ʚ;g4HdHd|k 0Dppp@  <4dddd x 0T<4!d!d x 0T<___PPT10 26___PPT9{? $O  =}d5Verifying invariants in object-oriented programs 66(;K. Rustan M. Leino Microsoft Research, Redmond, WA, USA<)Vision  A# and Boogie: Programmer's view.!("(( Boogie: under the hood Boogie technology and research(Programming methodology model for writing code and specifications Inference abstract domains over heap structures Verification-condition generation formulas that are  efficient for theorem prover * &"1* &"1iInvariants: straw manZclass T { // field declarations ... invariant J ; T(...) requires P modifies v ensures Q { & } method m(...) requires R modifies w ensures T { & } & !0P2!   lInvariants, examplerclass T { private int x, y ; invariant 0 f" x < y ; public T() { x = 0 ; y = 1 ; } public method m() modifies x, y { assert y-x g" 0 ; x = x + 3 ; y = 4 * y ; } & V!0P2  &!  " (,v+mInvariants, problemsrclass T { private int x, y ; invariant 0 f" x < y ; public T() { x = 0 ; y = 1 ; } public method m() modifies x, y { assert y-x g" 0 ; x = x + 3 ; y = 4 * y ; } & 4!0P2  " !  " (,v+qInvariants, problemsrclass T { private int x, y ; invariant 0 f" x < y ; public T() { x = 0 ; y = 1 ; } public method m() modifies x, y { assert y-x g" 0 ; x = x + 3 ; y = 4 * y ; } & 4!0P2  " !  " (,v+nInvariants, problemsrclass T { private int x, y ; invariant 0 f" x < y ; public T() { x = 0 ; y = 1 ; } public method m() modifies x, y { assert y-x g" 0 ; x = x + 3 ; y = 4 * y ; } & 4!0P2  " !  " (,v+pInvariants, problemsrclass T { private int x, y ; invariant 0 f" x < y ; public T() { x = 0 ; y = 1 ; } public method m() modifies x, y { assert y-x g" 0 ; x = x + 3 ; y = 4 * y ; } & !0P2  " !   " (,v+r'The problem of specifying modifications((( class Kitchen { private Dishes d ; private bool hasGarbage ; private Stove s ; private Light l ; ... public method SpiffUp() modifies hasGarbage, s.foodPieces, s.big.sufaceColor, & { d.Clean() ; hasGarbage = false ; s.Wipe() ; l.TurnOff() ; ... }!P     - >     s'The problem of specifying modifications((( class Kitchen { private Dishes d ; private bool hasGarbage ; private Stove s ; private Light l ; ... public method SpiffUp() modifies hasGarbage, s.foodPieces, s.big.sufaceColor, & { d.Clean() ; hasGarbage = false ; s.Wipe() ; l.TurnOff() ; ... }!P     2P- >     t'The problem of specifying modifications(((class Kitchen { private Dishes d ; private bool hasGarbage ; private Stove s ; private Light l ; ... public method SpiffUp() modifies { d.Clean() ; hasGarbage = false ; s.Wipe() ; assert hasGarbage ; l.TurnOff() ; ... }>!P     8& - >   jSoundness of verificationSoundness = verification finds all errors Soundness follows from: pre- and postconditions are the same for caller and callee Note: In addition to soundness, we want something usable>B;: B;:,K;u Methodologyobject invariant declaration class T { int x, y ; invariant x < y ; special variable st: {Invalid, Valid} Idea: program invariant ("o e o.st = Invalid (" Inv(o)) st is changed by commands pack and unpack)$  .   b(-4,vpack and unpackpack o a" assert o.st = Invalid ; assert Inv(o) ; o.st := Valid unpack o a" assert o.st = Valid ; o.st := InvalidD$6$ 2  !b   wExampleTclass T { int x, y ; invariant 0 f" x < y ; method init(t) requires t.st = Invalid modifies t.st, t.x, t.y ensures t.st = Valid { t.x := 0 ; t.y := 1 ; pack t } method m(t) requires t.st = Valid modifies t.x, t.y { unpack t ; t.x := t.x + 3 ; t.y := 4 * t.y ; pack t }+!P  "  ,,: '   xProgram invariant("o e o.st = Invalid (" Inv(o)) x := new(T) a" ... ; assume x.st = Invalid pack o a" ... ; assert Inv(o) ; o.st := Valid unpack o a" ... ; o.st := Invalid o.f := E a" assert o.st = Invalid ; ... Inv(o) can mention only the fields of o ,"%PP$PP!&  "  ""      F$"$((,",$  $yMethodology, summaryFinvariant ... st: {Invalid, Valid} pack, unpack modifications of o.f require o.st=Invalid Inv(o) can mention only the fields of o ("o e o.st = Invalid (" Inv(o))|$ R!$t1  *{Methodology, extendedcomponent declarations class Kitchen { component Stove s ; st: {Invalid, Valid, Committed} Idea: program invariant ("o e o.st=Invalid (" (Inv(o) '" ("p"Comp(o) e p.st=Committed))) pack o and unpack o change st for o and o's components%$ $e ?$  :J"   <>) |pack and unpack, extendedpack o a" assert o.st = Invalid '" Inv(o) ; assert ("p " Comp(o) e p.st=Valid) ; o.st := Valid ; foreach p " Comp(o) do p.st :=Committed ; unpack o a" assert o.st = Valid ; foreach p " Comp(o) do p.st=Valid ; o.st := Invalid ;$]$ 2" "  " "       $"$((((,",0000000000 4"48888 <"<   %  }Exampleclass Kitchen { method SpiffUp(k) requires k.st=Valid & { unpack k ; k.d.Clean() ; k.s.Wipe() ; pack k } v!&P   ~Exampleclass Kitchen { method SpiffUp(k) requires k.st=Valid & { unpack k ; k.d.Clean() ; k.s.Wipe() ; pack k } v!&P   Program invariant("o e o.st=Invalid (" (Inv(o) '" ("p"Comp(o) e p.st=Committed))) x := new(T) a" ... ; assume x.st=Invalid pack o, unpack o o.f := E a" assert o.st=Invalid ; ... Inv(o) can mention only the fields of o and of o.p for any component field p A%@$Z@&  "  k"*Extended methodology, summary(invariant ... component ... st: {Invalid, Valid, Committed} pack, unpack modifications of o.f require o.st=Invalid Inv(o) can mention only the fields of o and of o.p for any component field p ("o e o.st=Invalid (" (Inv(o) '" ("p"Comp(o) e p.st=Committed)))$ZDl sZ  wC&<  *!Verification systemWe let st be used in method specifications (requires, modifies, ensures) We must address the Problem of Specifying ModificationsN,:xh A heap modelHeap is a two-dimensional  array class T { f: U; g: V; ... } x := o.f = x := Heap[o, f] o.f := E = Heap[o, f] := E`#!8#  PF   Meaning of modifiesmodifies w = modifies Heap ensures ("o,f e Heap[o,f] = Heap0[o,f] (" (o,f) " w0 ) i$ ( ( >/ Meaning of modifiesmodifies w = modifies Heap ensures ("o,f e Heap[o,f] = Heap0[o,f] (" (o,f) " w0 (" Heap0[o,alloc] ) s$ ( (  (  >/Meaning of modifiesmodifies w = modifies Heap ensures ("o,f e Heap[o,f] = Heap0[o,f] (" (o,f) " w0 (" Heap0[o,alloc] (" Heap0[o,st]=Committed ) $ ( (  ( ( >/:Exampleclass Kitchen { method SpiffUp(k) requires k.st=Valid modifies k.hasGarbage { unpack k ; k.d.Clean() ; k.hasGarbage := false ; k.s.Wipe() ; assert k.hasGarbage ; pack k } !@"      Another examplejmethod m(p) requires p.st=Committed { var y, z in y := p.x ; z := sqrt(49) ; assert y = p.x end }k!Z" b " Soundness^Pre- and postconditions are the same for callers and callees, so verification system is sound!, # Related workDrep types in CLU dynamically checked invariants in Eiffel valid idiom in ESC/Modula-3 universe types and invariants in Muller's thesis invariant declarations in ESC/Java and JML (implicit) pack/unpack operations in Vault and Fugue capability calculus ownership types locking and monitor disciplines in concurrent programming:Px$PP:>"  -} ConclusionsInvariants different from pre/post-conditions Resulting program invariants hold at every program point Uses pack/unpack commands, but good defaults can be constructed for these No linear type system Components are not unique references objects (pointers) can freely be copied Fields can freely be read No additional features of abstraction needed to support the specification of modifications SoundZFurther research challenges(lexperience, understanding of limits extensions to support more good programs (joint work with Peter Muller) !  0` fp=` f3` 33f` 3f33` 3f3f` fff3` f3` 3|f>?" dd@,|?" dd@   " @ ` n?" dd@   @@``PR    @ ` ` p>> 4"(    BW CfDE,F6 W  Pn n /Hf  W W @`""  S D "`  T Click to edit Master title style! !   C 0 "  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  C  "``  F*0  C ( "`   H*0  C  "`8  H*0  B_ CwDE,F6  12w  _  `@`"55^   B C DE F*    FRj @`"%wT \5O % "5\O &B ZBC DEF!!T | ? s OOCi3[~d|YAdzu H  T T DH@`"\< ) 'B ZBC DEF!!T | ? s OOCi3[~d|YAdzu H  T T DH@`"5O x T 9B ( "9B b 9B )# "9B * BC&DE F*{ V&Ox{ { @`"T\ 9B + "9B , B\C]DE$F. *]\g @`"t9F - B(CDEXFb`M;Bl (TDAkl`^tZ?v.0@`"d . BC DEF" =@`"6zsn / 0B CDElFv_  5  o } 6 +   N ? T iS/x9 h  r [  u _ _ 8<@`"B 0 BCVDE F*PjV!rPP@`"iC 1 BCDE F*NT~(rFNN@`"( 2 BCDE F*N<:W6NN@`"v 3 BCDE F*X425+XX@`"iy,hB 4 s *DԔ"T0B  s *޽h ? fp=___PPT10u..o@$+D=' = @B + Crayon on right1  0` fp=` f3` 33f` 3f33` 3f3f` fff3` f3` 3|f>?" dd@,|?" dd@   " @ ` n?" dd@   @@``PT    @ ` `p>> &--p44,(    BW CfDE,F6 W  Pn n /Hf  W W @`""  S H; "`` ; T Click to edit Master title style! !   C (; "  ; RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  C ; "`` ; F*0  C <; "`  ; H*0  C ; "`8 ; H*0  B_ CwDE,F6  12w  _  `@`"55^   B C DE F*    FRj @`"%wT  i   " iV   BCDE`Fj3R3[J3d =xjXy.|7 sb"3324@`" Y:   BCDEF"x@`" E   B2C5DE0F: 3~25Fy+**. @`",X  BCDE F*ENEE@`"V  BCDE F*$ @`" lE  BCDEF"H@`"C  BCDE F*PWPP@`"  BC\DEF&j\+@`"  B8CDEFN8 @`"[mb  i # " ib   # "   B9CDE(F2 kr $9[CJe kk@`"Z  BC DE$F. ( G((@`"|)  BWCDE$F. $],PWt.@`" _  BCDEF"d4dd@`"L  BC(DE@FJ"BDF2Pk(x"""$@`".  BCDE(F2 [PjGaX9@`"5`Nb  iH # " iH  BCDE F*n(BPgTnn@`"'`  "BCpDEhFr?4CfcCPp(Y**.:(sk6Pg_68@`"OH  BCODE$F. tj!:^OLtt@`"ja   BCDE8FB|Q&9+Cca=wJL2 @`"  ! BCDE,F6 Lq>thc;?@`"BB> " BC DE4F> )B@  tMY)) @`"H.  # BCDE4F> _N95_}H9 @`" i $ BCDE@FJ~Bt*n Lp_55 n~~~"$@`"lT \5O % "5\O &B ZBC DEF!!T | ? s OOCi3[~d|YAdzu H  T T DH@`"\< ) 'B ZBC DEF!!T | ? s OOCi3[~d|YAdzu H  T T DH@`"5O x T 9B ( "9B b 9B )# "9B * BC&DE F*{ V&Ox{ { @`"T\ 9B + "9B , B\C]DE$F. *]\g @`"t9F - B(CDEXFb`M;Bl (TDAkl`^tZ?v.0@`"d . BC DEF" =@`"6zsn / 0B CDElFv_  5  o } 6 +   N ? T iS/x9 h  r [  u _ _ 8<@`"B 0 BCVDE F*PjV!rPP@`"iC 1 BCDE F*NT~(rFNN@`"( 2 BCDE F*N<:W6NN@`"v 3 BCDE F*X425+XX@`"iy,hB 4 s *DԔ"T0B  s *޽h ? fp=___PPT10i.o@$+D=' = @B + Crayons @ 0 (    BC#DEF" y#e  @`"   <;3 Ԕ8c?"` P  ; T Click to edit Master title style! !  C ; " p  ; W#Click to edit Master subtitle style$ $  C ; "`` ; F*0  C ; "`  ; H*0  C X; "`  ; H*0T {   "{    BCDE0F: >,GS:@`"{    B2C5DE0F: 3~25Fy+**. @`"j    BCDE F*ENEE@`"X\ {    "{    BCDE F*n(BPgTnn@`"|f  (BCpDEhFr?4CfcCPp(Y**.:(sk6Pg_68@`"{   BCDEF"d4dd@`"D  BCODE$F. tj!:^OLtt@`"|  BC(DE@FJ"BDF2Pk(x"""$@`"NT z N[   " zN[   zBCDE0F: >,GS:@`" E   zB2C5DE0F: 3~25Fy+**. @`" 5   zBCDE F*ENEE@`"  \ z N[   "z N[   zBCDE F*n(BPgTnn@`"zw  f  (zBCpDEhFr?4CfcCPp(Y**.:(sk6Pg_68@`" [   zBCDEF"d4dd@`"Z!    zBCODE$F. tj!:^OLtt@`"U N   zBC(DE@FJ"BDF2Pk(x"""$@`"= L $  C BCDELF$)+,04k|w@xy( @  E@      "p 8;   B0CDE(F| fYc 0 @   " 8 B  s *޽h ? fp=80___PPT10.o@$? 0 zr` (    0q; P   ; P*    0Tv;    ; R*  d  c $ ?  ;  0hy;  0 ; RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  64ߒ _P  ; P*    6; _  ; R*  H  0޽h ? 3380___PPT10.ABA 0  0(    <L<   ^Joint work with Mike Barnett, Robert DeLine, Manuel Fahndrich, and Wolfram Schulte_ _x  c $ <p < x  c $ <P  <   0< Q f2Computer Science Colloquium ETH Zurich 24 Nov 20033 23  0@<x 8  :%  2# H  0޽h ? +T3f3f___PPT10i.@ n@+D=' = @B + @ 0  <(  <~ < s *)``   . < 0,k<  p  b Record design decisions + Utilize automatic checking = Detect errors and improve maintainability,c7*|F HB < ND>?"0@NNN?N@ @H < 0޽h ? ffNL|>rL___PPT10i.CPSiO+D=' = @B + @ 0  4:(  4RB 4 s *D0 D ~ 4 s *,``    4 <h<  T  :Boogie RB 4 s *D D  4 <<$  ? C# compiler   RB 4 s *D)  4 <<P ? A# compiler   RB  4 s *D dp  4 0t<9 <A# 2  4 0؞<iT  <C# 2  4 0<9   >MSIL 2  4 0<Y $4 BWarnings 2 RB 4@ s *D@ P R  4 <<` @ HOther .NET compilers RB 4@ s *D"H 4 0޽h ? fp=  ___PPT10 .0>:+D ' <= @B D' = @BA?%,( < +O%,( < +D' =%(%(D' =%(Da' =4@BB BB%(D' =1:B 0.5*3>%Bstyle.opacity= B PPT<*4D' =-6B image0BIE*v3=2Bopacity: 0.5 BIE<*4Dn' =A@BB BB0B%(D' =1:B 0.5*3>%Bstyle.opacity= B PPT<*4D' =-6B image0BIE*v3=2Bopacity: 0.5 BIE<*4Da' =4@BB BB%(D' =1:B 0.5*3>%Bstyle.opacity= B PPT<*4D' =-6B image0BIE*v3=2Bopacity: 0.5 BIE<*4+8+0+40 +i  @ 0  x 8 (  8RB 8 s *D@ p 8 3 BhCPDEF<,hX P@  `@ x 8 c $<plTp  <  8 <<<  dTheorem prover RB 8 s *D  8 <<P   Rweakest-precondition generator RB 8 s *D@i.  8 <8<GP > translator   RB  8 s *DW`  8 0d<p, >MSIL 2  8 0P<B \ \BoogiePL 2   8 0h< ]   Tverification condition 0 P2 8 0x< 0' BWarnings 2  8 <l<P  DInference engine RB 8 s *Dp` 0  8 C BvCDE(F BK6ly$L8cvx @    H 8 0޽h ? fp=___PPT10i.ap+D=' = @B + @ 0  D0(  Dx D c $<P   < x D c $l<0  < H D 0޽h ? fp=___PPT10i.GPۜ0+D=' = @B + @ 0  p (  r  S H<``  <   S ,   < D  C p   Zclass T { // field declarations ... T(...) requires P modifies v ensures Q '" J { & } method m(...) requires R '" J modifies w ensures T '" J { & } & x!0P2+&   & &  0 9` ]Object invariants hold on public method boundaries and are shorthands for pre/post-conditions^ 2^; H  0޽h ? fp=___PPT10i.r+D=' = @B +# @ 0 :2 (  x  c $ ;``     c $6 (  ^B  6DY j r  S <``     S P9 @  $   C  @   class Stove { private Burner big ; private Burner small ; private int foodPieces ; private Knob[] knobs ; ... public method Wipe() modifies foodPieces, big.surfaceColor, & { big.Polish() ; small.Polish() ; foodPieces = 0 ; ... }!Z  iE A       0 @P  l4these lists are long, and they mention private state5 25^B  6D p H  0޽h ? fp=___PPT10i.rP;+D=' = @B +) @ 0 @8@ (  x  c $``     c $<9 @  $   C  @   class Stove { private Burner big ; private Burner small ; private int foodPieces ; private Knob[] knobs ; ... public method Wipe() modifies foodPieces, big.surfaceColor, & { big.Polish() ; small.Polish() ; foodPieces = 0 ; ... }!Z  #EE A     v  0\ ~ possible solution (?): don t need to declare modifications of private state it can t be observed anyhow*i 2SH  0޽h ? fp=___PPT10i.rP;+D=' = @B + @ 0 P [(  x  c $``     c $9 @  $   C 8% @   }class Stove { private Burner big ; private Burner small ; private int foodPieces ; private Knob[] knobs ; ... public method Wipe() modifies { big.Polish() ; small.Polish() ; foodPieces = 0 ; ... }!Z  EbE L    >  0&P  zSpiffUp treats Wipe as if Wipe modified nothing, so what if Wipe calls a method in Kitchen that sets hasGarbage to true?! { 2{$^  H  0޽h ? fp=___PPT10i.rP;+D=' = @B +>  @ 0  P(  r  S `P`     S 0 <$ 0  H  0޽h ? fp=&  ___PPT10 .r{ +!lD ' = @B DU ' = @BA?%,( < +O%,( < +Da' =%(%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<**%(D' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<**B%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*B}%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*}%(+8+0+0 + @ 0 ` ](  r  S ``     S D`P     0P9L   sholds at every program point!: 2 l  09,  Vfor any o: T, we write Inv(o) a" o.x < o.yT,  %!>dB @ <DjJ0` PdB @ <DjJ @ H  0޽h ? fp=___PPT10i.r0+D=' = @B +} @ 0 p $(  r  S x``   r  S P   H  0޽h ? fp=___PPT10i.s+D=' = @B + @ 0  (  r  S 0``     S " :   0$r Bk \receiver parameter ( this ,  self ,  current )/ 2/RB @ s *D H  0޽h ? fp=___PPT10i.s;+D=' = @B +  @ 0  P(  r  S 4:``     S : <$ 0  H  0޽h ? fp=___PPT10 .8s)+!lD| ' = @B D7 ' = @BA?%,( < +O%,( < +Da' =%(%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*"%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*"O%(D' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*O%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(+8+0+0 +} @ 0  $(  r  S D-``   r  S -   H  0޽h ? fp=___PPT10i.;sV'+D=' = @B + @ 0 2*  (  x  c $B``     c $S`    h  0TUP 0 Rfor any k: Kitchen, we have k.s " Comp(k)f* %%!,   S BCDEFHC"+D@  c"$` pn 0H  0޽h ? fp=___PPT10i.r0+D=' = @B + @ 0  F(  x  c $,lp     c $}P  "1H  0޽h ? fp=___PPT10i.s+D=' = @B +] @ 0 ?7  (  r  S pp     S D:`  $   0: ` $lclass Stove { method Wipe(s) requires s.st=Valid & V7 2  ,    zB C@DE FA@ @@S"   `2  # l?x c Z<"`0  f,$@ 0!   C xУ:?"`C H ,$D 0 7s !   C x{?"`n ,$@ 0 7d    0Z 9 A,$ 0 ?Kitchen( 24   # BC DE(FA 8px`HP@ @   S" P 0p,$D  0   04@p',$ 0 5k 22  # l?x c Z<"`pp` ,$@  02  # l?x c Z<"`  ,$D 0  0p  ,$  0 =Stove( 2  0n:9 d ,$  0 >Dishes( 2  # BCDE(FAA  0`P P @   ` P ,$@   0  # BCDE(FAA |T(PXhxpph @     ,$D   0  0U,$D 0  00@ P,$ 0 AValid ( 2  04 r1 ,$ 0 E Committed ( 2   0 ,$ 0 E Committed ( 2   S ~?|"``0 ,$@ 0 .   S ~?|"`N @ ,$@ 0 .   S ~4?|"`W ` ,$D 0 .   # B`C@DE(FAA @PP@T` @   K0,$@  0  # BC@DE(FAA @\( Ph @    P0 ,$@  0  # BCDE(FAA H4h H|T @    p0 ,$D  0  0`,$ 0 C Committed 2   0\ ;; ,$ 0 C Committed 2    0x0 ` ,$ 0 C Committed 2 H  0޽h ? fp=\ATA___PPT104A.Js+SKnD=' = @B D{=' = @BA?%,( < +O%,( < +D<' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =+4 8?dCB0-#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =%(D7' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =-s6Bwipe(left)*<3<* D' =%(D+' =4@BB BB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =-g6B fade*<3<* D' =%(D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =-g6B fade*<3<* D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =-g6B fade*<3<* D' =%(D7' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-s6Bwipe(left)*<3<*D7' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-s6Bwipe(left)*<3<*D6 ' =%( D+' =4@BB BB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D+' =4@BB BB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D' =%( D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D ' =%( D7' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-s6Bwipe(left)*<3<*D7' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-s6Bwipe(left)*<3<*D7' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-s6Bwipe(left)*<3<*D ' =%(D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =-g6B fade*<3<* D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*+H+0+ 0 ++0+ 0 ++0+ 0 ++0+ 0 ++0+0 ++0+0 ++0+0 ++0+0 ++0+0 ++0+0 ++0+0 ++0+0 ++0+0 ++0+0 ++0+ 0 +1C @ 0  !!&(    00@ P,$ 0 AValid ( 2  0T:3@ S,$ 0 CInvalid ( 2x  c $     c $`  $   0' ` $lclass Stove { method Wipe(s) requires s.st=Valid & V7 2  ,    B C@DE F@ @@S"   `2  # l?x c Z<"`0  f  C x)?"`C H  7s   C x:?"`n  7d    0l,Z 9 A ?Kitchen( 2   3 BC DE(F 8px`HP@ @   S" P 0p   01@p' 5k 22   # l?x c Z<"`pp` 2   # l?x c Z<"`    0@6   =Stove( 2  04:9 d  >Dishes( 2  3 BCDE(F  0`P P @   ` P   3 BCDE(F |T(PXhxpph @     X  0U  0p> r1 ,$ 0 E Committed ( 2   0A ,$ 0 E Committed ( 2   S ~dE?|"``0  .   S ~|J?|"`N @  .   S ~L?|"`W `  .   3 B`C@DE(F @PP@T` @   K0  3 BC@DE(F @\( Ph @    P0   3 BCDE(F H4h H|T @    p0   0O` C Committed 2   0pT ;;  C Committed 2   0X0 `  C Committed 2    0\ r4 ,$ 0 AValid ( 2 ! 0_ ,$ 0 AValid ( 2H  0޽h ? fp=C(;(___PPT10(.Js+GbPDO%' i= @B D %' = @BA?%,( < +O%,( < +D' =%(%(D{' =%(D#' =4@BB*BB%()?)?Dw' =.?7 BBBBBQM 0.00052 2.22222E-6 L 0.00052 0.05069 *3>*B ppt_xB ppt_y=@0BBAApBBB@<<*D ' =%(D6' =A@BB BB0B%(D' =-g6B fade*<3<*D' =1:Bhidden*o3>+B#style.visibility<*%(D6' =A@BB BB0B%(D' =-g6B fade*<3<*D' =1:Bhidden*o3>+B#style.visibility<*%(D6' =A@BB BB0B%(D' =-g6B fade*<3<*D' =1:Bhidden*o3>+B#style.visibility<*%(D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =-g6B fade*<3<* D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*!%(D' =-g6B fade*<3<*!D' =%(Du' =%(D' =4@BB*BB%()?)?Dq' =.97 BBBBBKM 0.00052 0.05069 L 0.00052 0.18403 *3>*B ppt_xB ppt_y=@0BBAApBBB=<*D' =%(Du' =%(D' =4@BB*BB%()?)?Dq' =.97 BBBBBKM 0.00052 0.18403 L 0.00052 0.23472 *3>*B ppt_xB ppt_y=@0BBAApBBB@<<*D ' =%(D6' =A@BB BB0B%(D' =-g6B fade*<3<*D' =1:Bhidden*o3>+B#style.visibility<*%(D6' =A@BB BB0B%(D' =-g6B fade*<3<* D' =1:Bhidden*o3>+B#style.visibility<* %(D6' =A@BB BB0B%(D' =-g6B fade*<3<*!D' =1:Bhidden*o3>+B#style.visibility<*!%(D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*++0+0 ++0+0 ++0+0 ++0+0 ++0+0 ++0+0 ++0+0 ++0+0 ++0+ 0 ++0+ 0 ++0+!0 ++0+!0 + @ 0  \(  x  c $``     c $ @@<$ 0  H  0޽h ? fp=o g ___PPT10G .8s)+!lD ' = @B D ' = @BA?%,( < +O%,( < +Da' =%(%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*A%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*Ak%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*k|%(D' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*|%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(+8+0+0 + @ 0  0(  x  c $<:``  : x  c $:  : H  0޽h ? fp=___PPT10i.;sV'+D=' = @B +} @ 0 0 $(  r  S ``   r  S    H  0޽h ? fp=___PPT10i.SsR*+D=' = @B + @ 0 ` 6(  r  S p p     S 0``   H  0޽h ? fp=___PPT10i.rm+D=' = @B +[ @ 0 rj@  (   r   S l``      S :  "*   0 ; PT `(viewed as set of object/field-name pairs) 2)    BC DEFA 0`` 00@  c"$`   @    BCDE(FA `P8`8H @   c"$` @ p H   0޽h ? fp=___PPT10i.Tsx+D=' = @B + @ 0 P J(  x  c $:``     c $ : &*H  0޽h ? fp=___PPT10i.Tsx+D=' = @B + @ 0 ` J(  x  c $``     c $d;  &*H  0޽h ? fp=___PPT10i.Tsx+D=' = @B + @ 0 % !(  x  c $     c $   $   04';   /Mclass Stove { method Wipe(s) requires s.st=Valid modifies s.foodPiecesnN 2  >    B C@DE F@ @@S"   H  0޽h ? fp=___PPT10i.Js+D=' = @B +2 @ 0  (2(  (r ( S @``    ( S    H ( 0޽h ? fp=80___PPT10.{s`\`>} @ 0 p $(  r  S >``   r  S >   H  0޽h ? fp=___PPT10i.Vs>׵+D=' = @B ++ @ 0 B:@(  @x @ c $l ;0@(   x @ c $ ;@0  ;  @ 0?` :%  2#H @ 0޽h ? fp=___PPT10i.Mz+D=' = @B +! @ 0 80 (  r  S 0Y0@   r  S ]p    0X;d\  <%  2# H  0޽h ? fp=___PPT10i.RsX+D=' = @B + @ 0 4, ,(  ,r , S j``   r , S k    , 0b;XH? 8%  2!H , 0޽h ? fp=___PPT10i.}s4+D=' = @B +ra_Slp %Ը*K2 Hf"+4=<nDpW.]_csIvl{~G-s0PM5:=GH@ ^EyPPifJSwOh+'0` px  $ 0 < HT\<Technologies for finding errors in object-oriented softwareRustan LeinoRustan Leino109Microsoft PowerPoint@t@@h@@@?mGg   `  y--$xx--'f--$n Uv%n--'--$ C<0  1 ;B!C--'--$ 8<C"B#9"1"  --'--$ 1#26 --'--$<97:;=<--'--6$  1!; C"E>;9<A;348410   --'--$ 73  --'--$   --'--"$$($")*'--'--$ [ZXQPOOVYZ[--'p=--$ QYYZZXVNOPQ--'--$OVWYRQO--'--$ZYXYYZZ--'--6$QPONVYZ[ZZZZZYWXYXWVOOPRQ--'--$RZXQR--'--$RQPPPQSR--'--"$STUVUSSSTVVVTSS--'p=--`%.XYZ[\ ^#_&_)_,_1^6\9\;\<\=]>^?_@aAbBbCbDbEaG`H_J^L]N\P\T]X^\_aaebjcndreudxc{b~a_^]\--'--&%G"I#K$M%O%O%P%Q#R"S"S"T"T#U%V'V'V(--'2HGPSoeiKakupoptai-. 32 Q3Joint work with Mike Barnett,c."System:-2HGPSoeiKakupoptai-. 72 V8 Robert DeLine, Manuel Fahndrich,.-2HGPSoeiKakupoptai-. $2 [=and Wolfram Schulte.-2HGPSoeiKakupoptai-. *2 /Verifying invariants in.-2HGPSoeiKakupoptai-. 2 9object.-2HGPSoeiKakupoptai-.  2 98-|.-2HGPSoeiKakupoptai-. "2 9>oriented programs .-2HGPSoeiKakupoptai-. *2 0Verifying invariants in.. *2 /Verifying invariants in.-2HGPSoeiKakupoptai-. 2 :object.. 2 9object.-2HGPSoeiKakupoptai-.  2 :8-|..  2 97-|.-2HGPSoeiKakupoptai-. "2 :>oriented programs .. "2 9=oriented programs .-2HGPSoeiKakupoptai-. "2 B$K. Rustan M. Leino.-2HGPSoeiKakupoptai-. =2 H)$Microsoft Research, Redmond, WA, USA.-@"Tahoma-. 02 i Computer Science Colloquiumr.-@"Tahoma-. 2 m ETH Zurich.-@"Tahoma-. 2 r 24 Nov 2003.-2HGPSoeiKakupoptai-.  2 Ued.-՜.+,D՜.+,    5On-screen ShowMicrosoft CorporationT % ,ArialHGPSoeiKakupoptaiTahoma WingdingsSymbolCrayon on rightCrayons6Verifying invariants in object-oriented programs Vision!A# and Boogie: Programmer's viewBoogie: under the hoodBoogie technology and researchInvariants: straw manInvariants, exampleInvariants, problemsInvariants, problemsInvariants, problemsInvariants, problems(The problem of specifying modifications(The problem of specifying modifications(The problem of specifying modificationsSoundness of verification Methodologypack and unpackExampleProgram invariantMethodology, summaryMethodology, extendedpack and unpack, extendedExampleExampleProgram invariantExtended methodology, summaryVerification system A heap modelMeaning of modifiesMeaning of modifiesMeaning of modifiesExampleAnother example Soundness Related work ConclusionsFurther research challenges  Fonts UsedDesign Template Slide Titles%D 4<Version $_rT Rustan LeinoRustan Leino  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Root EntrydO)Current UserSummaryInformation(PowerPoint Document(TDocumentSummaryInformation8