ࡱ> za.Hy]_{`@U( f3f3uY( 6/ 0J5DHGPSoeiKakupoptaip0h 02^4^43 LPl(Uq$HGPSoeiKakupoptai HeavyVer.2.02"HGPSoeiKakupoptaiBSGP޸22ƀ%X fd<*+-?8,M)llI 6ɩ 4n18ɳ)|YBEbYγYfaa//фBVN;RI6VwY.֥ Mtغ&D@7(_'sʍa=/8ϻٶ8iHTYy l,J%G*y'^A+of P^K#'3xtGsY_W-lXQ<8nq>G* q;U @ǠФAS,ӏX4TDA.Qݓ `DW875Ni3MzEWp`W~b꽂$yWFg K0D&> &~Bm#aILi2d$$2|0~qOj,N1&pP20jH^@ं&zIA˯gX%浔V5!(W*ƮS:6t{:+uq|7>7-q˦ 0TΙt;B:LaCRt f!ua hƖ|0ľQDC!45C21<ݖ&F$8G!ٰe D 'y$3< <ӆ5/$0 i8+®< iiFa->Iڛ#U:ϳMV>l^گY^ueux}Ͳu`v_^Wauc5׍w}7zYH290"af&&jh5T؛2rn9`l-hl6ڛ[lmx.ۢrɢٺK;f[x޷7:[KNp2}pSL)Ÿ#96u29NY29w0QHͺ9$F$L֥DR%:^;$ݣL IHgy0;E#Jٴ+kL?ߣ>Äts~O?pb 9A BD(sXhx,J2ӌHđ I%bMO2l/ 8'$^d~0 0)x/DFD);'ۂTHH 2U `0@"'ǮSJ`!hRUA5€a RR ISIN)EH29 XY+ElҼW0"Y"Z H-E2yp.%ȹr6 xz2d9ȋ3bm\s/"8ˉrH2*feP?77Ӭ; Q`#Di 3D[ϳ8<4GE0{>Dpf@BLB ABH!D,%Hy"$Hb)#䀒gDf!4DT `<1ج ?Fn:@CPjQH1#MHLQ7GL !5L<ĉ$&<AH?Yr anr̶ICIdc=pz;ѓÈO8=/>86azPݥ²1AܺlA9o0 {4݅{: ̯0_B`X '$$+oB2؞}LiJ? c'$:2t}$rЅx{cύ 𔊹|fuȁ")ǪuFԙ x,`OhZͥ M߼h!6 X2 [gfΆuNzkNO+'pMcW:S2QI$hxq~% \]# /?CO1m^R>?H͍6[x[hI'6,8>4JS$Nȧ\ebj˞"gVVOPE ;?@?Gq{ DV_(j^Y—& HޞzǷX'C0t>^D{0+RG$Ħ! (?ڄHI) 0:^H.> 0CfcY;q()UJ FG#` &FrAge%P| +@nD)"h&Cb| @~'U`*3ـ\ȼ(- }#|1bO,&8l\+ ft%ƚm91-B®N%3Ksy'Ȓ^iG+@;o;8X\S˟ּїNPlxNb^􇀱 pīd #y`*|[6$f7wؒY}6cU$IÜQwvRTy B$ݬ{&>XHaK^Wς@ZLج@.c#2v)->,G<0Dq!t2HG<-L#H u89ȈzS?tg(;sJQf(.FBbFb89:z t߭QujAԓ-v`N^.Y/?;SԸOL*=Bx0 cSŊ?jRg#)}(`Ob␽D]+*uEA\f$o"n*Q`Niu 錽>I7ltPѪ]{~wO q'h._^ɐ|?D'pa~v`*W򻝳r4|ÑhCܒ]OXs8l 2G->!ԑ \<;'KڈazԷi0Y 4d 4RJyM.L5 <&8SÉaA". %0%؇IidlAt蛮(T0h`"IퟧⲢHLKm|D!,K^ ?24`nzV ?Eal h@ dJ<zϲBOzxHְf DS))HXW2E1"h?jW?2^WBsFGSqhb"&Laaha{v5WECpةPٚ7y@^X=$G"As.Z2- 8n@TK:J ,oIT7)@&B,Ov W/V˅q0S* ݦg%XFdTla;F\!Mf4ЬNI3W"feo "rC rbzOVNħU"l@K xbd𪇈%Pe8xY{Y|?4@Byt i;; b_P0#}88]Գ T@Y T W.S*:j> B$=< *w`o#prAuEm(4ݚ ME湀.槃c)pe}_跐T&cR47W(reAԪQU.L0ݹe=f{KeJCh=ml+*e u,@$WǡO'ka9zT5*OvI]QO5pCQ{&5p|ռth#ho\'MÓM;6epVrUwqѱ*PĚ&P2!CrO65vKUc3CK# P1sFDt_D?GY^-:z48cb Y)x*jze(1u34a\,62sW$51rw)oGcWjf$m3) T,`h4y~m Щ1~Ul'+:vgMŶ2[Lz]?ZZkW݆jC_K 3aqtqWѮ?]ai9!6+@_g "?=a˔Dz"dr.&>i.hܡ!n(dVMt˒s 6e%Kf0v"r[B<Y2/C0%@9V *G,ӗ`\Vo XVc>/LFc.Gm;w"DڑL\ɪImW@(nzJfS/;J[4|ysTk{R4~9ŶGٕ>U PO^L>kcNFo@6S8س.qhf%II)zuv`UbLҌS%%TX>pi}mO<0?kg?T7W]V%7#pf? /2sU6x$AIv_/R? ~1$odLʲ,"b c:3 @n0௝$]@m&JZl0NLlk*,L&TI/Zl3$'ΰ'n`x]cJilD_ }6EU:lDy/AK|m%#PaU5dcZ5[xu2~AZՖ<Sl`*Sظ#GY7'3;q6LHUM-gl렎ѫYjyk<;41M@U}8bڻfҫ!ZAsg)-lSl{@70<]*UK uXH3]bUGMV'q!=@MլH@JS% b QXtɀZklLgd52w&HZZ]1f8!Ե|:5x3@(:] P a4ͰDc1j!Œe; c( LZ+̭"`vndd R0 EFErH;Aia0j,6V"wpx6Z@BÃdN<&-x Yh,?I<) E˲pZ~,V>uwN]2fPf"/dqS.Wuyٸv]Txu `+N{qDPإ[f*ivX gǁd}+aF V=+qӏ)\ 833[\h34/s\!4XQ&`T %T|:~Y€2"Źt_DS~D|Gl_<܁G0bHN㍫=v'c2dg\z VF83PoE# mM?dPQ ,7 35nmMfz0z50 TXW:j÷qV/` 0cf&z70N,`Zf=~;u xŋG%qa 7rC2O]=1jܬO\ *mr$¢yNg)20QQT%:5 ʞ[tZ Uya_Or{FEKˌ1_2r pv: 2 APY~w,V#`Bf/$l WQy-3#D SM?-K(~4 jXaŊӗ 'MwpRU%D %mR@@9&:&!|֏B}:z6RE$Yr` %r aSIi4E1w~$cZM wI%8J; h0vSMA͔Qsxi[Md #VՒ cȧ&G's3b72P: QQkBB0!to,ѼޟȂ^mD@` 3x^ [~\ @@eX8z<,4ʓJ%zt K*Q@xCU1pUϵh=BqV ѻB0}3 'G@Jș^Ys6AExY[ GX? Pı bcDA_ 7Uʅ}<Ehw`b-M,~ъxQ.F;A6` dgJ i(`s"KNO$Pe1a\swtzXƌ"DĔ/b"Sy"JH!'UG^,ӚN*AzPM~P `1lY/Pd3].KSv3Lx: R'Z^ɭim-(/AyP(Fx9Dt}6mh ~]iA(7v̲ rT&g}LZл5 n3bkJh5!@TtiRVrnk"[k!0rF#59rZNj(CB֍ݭD _`6PbbY~)3g -@K!(  !򹳩XG\ fl&&,P4F=􄁂 21&k ܷ P)a ZCȊ= '+('dkn:]}RGܻ8h2 cD +4?0*"{$ 71,[Aߏeâ#tq' ^ǎ1W,ұDVGT@j?Ɠ̀E&%9i>87ivw=4 32o@Ny,lvG©"UY!B`x, cw#*J\WRwю>/%!)qJ \@QFK#}NS.)>\ޟb|1O7"mlEP#1|{&o"?F`yy=e?߂ג2+o  _~+g'T,NAцB*(tw:GtF}pk_ +ͱӽ,U dK0T}qRڕ k@ULؙKɘm5# q`-@?1zDi!qp@C![H$< 1 hפ/I6b-tj+:dܡ[ "(,3z>_-N 4?fުV`%/\$G83iƗ4@ 7KU?S :Q-hYnKl"+z[ܩIO&P-O{ Ё$G6tw  ` C8# a 2-)|'/ ^DK|)}E:xq}v{{cU T*RUb*4څste& HCKV}n@H"y*10 肑'I{WUCp.p.@-rS]7k9PmXDc&5gd&L,_C'v]u[USUQ (~ BS{H*4J[rR$M I@F"o,d=*Y9Des*=%V BEp$KIH FCT|z;c<L` "^'! { .`|'H1%.`J<W z(o/,CP P#0HVp 3@0\@<iž|y+uyp/_Zt;Fx^,ɇ1cSas,~k0s;0p`_2_uk-2NV[efZ,2PeK:YeC:٩M׃T΋Ck|ڌJwhšjoɏ+LS$˻/2e͡"ɴ%=6f'b7$ek([acTі7($ B1@!oq r> 'o 0|n!ޱzNpt% x.Uq7듓8NpCU3:]]CRYrVv#zM^ul=:؛E0-5 gcV=c֓kGa'1Y†yv[6\{0(4a)Me]*1RuTP (bJܯuTZujWU-Pl#Q,h+Z-X+P%- RCť+)F&&QBD|#1$(B9PAF$bP2J&j>9C"* ~@Rac+A'Rrmy0aPqcEg2i{#1qr\\N,jFG$⓴5L,zfX8f4FW1 qs0ܦ;a|SNUa8bG\Cr)A.KSRđ6KK˜`̭%BF.ZlUTeh8]]ĮD*Gd%!'+aDXRQ-r'aVH:"q9 |Kwؘ-:H60ApJb}8FB8P%E{={Dq BJHw;,.1c<߽{n^k>{v/yGҞ.ȝ7vtJy].?_ * |hmcB)DA2DS)9E3hJ Nz`j*u6k bҐ868۷685ۨ"*ΛC$iʨcPǛ0I#.%D! vp̜.wET&JALLԌx&N68DDAtrGV(dL~獙t,!"M3MT x^&^-"PA'V(E >;=d,e%a(ٯJTt¦vXJa`0'a'Cy&_v38D8EqI=1zA<4C2(Ql&"T! `OO!_ (fFLahj #TJҥ׈]hQT. B%Ej8'qC@a41]R+4-Bfcrdj0ucjI6hcT̚LBhdã;d cKLJK7)ą]0Ԣ4̑%ЬI=K뼘uܠ?u 2h==cL%b$嚐 fC[ge,Ard?=:[Ѷ6dUBHn jI3sdA[G/p;볊 ƸܦiݦY`2MF&jU` =. ZOǑdڲV15uȌǁ|İBCRV`S KA]W]D`1غ WiQ(D00#cW-ӛ"vRE1|nT@|hZw+ Hnޠͦ%gofXlxnx]?3/9.];'|&wǪy< @@#XApZM-pf V5[h(<RM0E=U@>5vFuK%v;L,W+Ǖ cK]Jql 1nld/c))B㚀Eٳ"sfDWH7E*fK-ι%ls`J<ȱl0m@wb&WL ->)^NSHR B(̛@60.]^F9R5}(vObS1Na%Wd L2] Xj@asILq)uuCcip(H0݉mg23u ;r6(r@Ej3t,r e F <9sB(J' gMH[č. ;. !@B3GV[͗bP`_Dip>*؋qEeFmRj=팄6zQ0î.u=ҍM35$D1LԞG';n-bl#J R,XH\|>?butDArialiKakupoptaip0h 0" DArial Unicode MSp0h 0"@ .  @n?" dd@  @@``  (c  **>>()  *5+;  PQRS6TLW XYZ\*]$^ `%a$bd(/X$r$.Hy]_{`@Ui 0AA 3QfT@8 E-Emʚ;xum8ʚ;g4idid/h 0 ppp@ <4dddd<` 0p0<4BdBd<` 0p0<4!d!d<` 0p0 <___PPT10 2v___PPT9XP8?  %jDVerification of object-oriented programs with invariantsEE(pMike Barnett, Robert DeLine, Manuel Fahndrich, K. Rustan M. Leino, Wolfram Schulte2qZ8- ;Example problemX class T { int x, y; invariant x < y; public void m(U u) { x++; u.p(); y++; }|Y!  $> '"Wanted: Methodology for invariants# (Ideal methodology: easy to understand statically and modularly checkable identifies all errors in a program permits all good programs bYo&m&Y PInvariant declarations  one per subclass)( class W extends V { int a; int[ ] b; invariant a d" b.length; & F!  ">6Special field inv keeps track of which invariants hold,7((&(Declarations and statements of programming language determine when inv is changed The associated invariants are checked when inv increases To prevent established invariants from having to be re-checked, one can treat fields in and below o.inv as read-only^PC7p(inv can be used in method specifications")(&( class T { int x, y; invariant x < y; public void m( ) requires inv == T; { int[ ] a = new int[y-x]; & }(!O! 2   > F  (inv can be used in method specifications")(&( class T { int x, y; invariant x < y; public void m( ) requires inv == typeof(this); { int[ ] a = new int[y-x]; & }(!Z! 2  P >   Exposed vs. owned Components  Components\Component fields are declared as such Component fields are not necessarily unique references6&$Z7Z 3T ComponentsWhen inv is increased to U, then U s components are checked to be consistent (p.inv == typeof(p)) and are subsequently un-exposedDH/,N# ComponentsZDecreasing inv below U exposes U s components4.  3Fields of components can be mentioned in invariants44(  License to modifyA field o.f can be modified only when o.exposed holds A method m is allowed a net effect on a field o.f (including o.inv and o.exposed) only if: o.f appears in the modifies clause of m, or o was not allocated on entry to m, or o was not exposed on entry to m`R$ $ $   #t 5   o 4Method calls may change fields of un-exposed objects55(   Related workrep types in CLU valid idiom in ESC/Modula-3 (implicit) pack/unpack operations in Vault and Fugue capability calculus ownership types invariant declarations in ESC/Java and JML locking and monitor disciplines in concurrent programmingP$PYP+$P:Pp \  ConclusionsSimple! inv, exposed, identification of components, protocol for changing inv/exposed object references can always be copied but objects can have just one owner fields can always be read but curbed expectations about the values read frame problem solved without abstraction (e.g., data groups) Want: experience, understanding of limits extensions to support more good programs more detailed comparison with other work"PN$P'P$PP.P=PvP 3$'$  .  =v1  0` fp=` f3` 33f` 3f33` 3f3f` fff3` f3` 3|f>?" dd@,|?" dd@   " @ ` n?" dd@   @@``PV    @ ` `p>> t-l-44 -(    BW CfDE,F6 W  Pn n /Hf  W W @`""  S  "  T Click to edit Master title style! !   C ܉ "   RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S  C  "``  `* b  C ԕ "`   b* b  C  "`8  b* b  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=80___PPT10.G K Crayons  0 5-(    BC#DEF" y#e  @`"   <T3 Ԕ8c?"` P  1 T Click to edit Master title style! !  C 1 " p   W#Click to edit Master subtitle style$ $  C 1 "`` 1 \*   C t1 "`  1 ^*   C 1 "`  1 ^* T {   "{    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.G KB  0L0 A9  (  x  c $1X@  1 x  c $1 `P  1   01 HFormal techniques for Java-like programs Darmstadt, Germany 21 July 2003(I 2Hb`   01 s 3  E( 2bH  0޽h ? 33___PPT10i.G0ۯ+D=' U= @B +  0  8y(  8r 8 S (  <r < S |8  8  < S Ԉ8  8 &@b:H < 0޽h ? fp=___PPT10i.lMЀ\+D=' U= @B +ͧ  0 ?7 @(  @r @ S 8  8  @ S 8 0 <$ 0 8 2 @ 3 r  Z<<P ` ` ,$@ 02 @ 3 r  Z<<P ` p ,$@ 02  @ 3 r  Z<<P` ,$@ 02  @ 3 r  Z<<P` ,$@X 02  @ 3 r?  Z<<P` ,$@   02  @ 3 r  Z<<P` ,$@  02  @ 3 r  Z<<P` ,$@ 0 @ 089   ,$ 0 :Object( 2 @ 01  w,$ 0 5Y( 2 @ 08  g,$  0 5X( 2 @ 08p  W ,$   0 5W( 2 @ 08i  P ,$X  0 5V( 2 @ 0@8P  7 ,$ 0 5U( 2 @ 08I  0 ,$ 0 5T( 2R @ 0 @ ,$@ 0B @@ s *Dp p,$@ 0` @ C 8  ,$ 0 f class V extends U { P p; invariant p `" null; & b4!  R @ 0 @ @,$@ 0B @ s *D p ,$@ 0 @ 08C"? ,$,  0 EY y = new Y(); 24 @ # BC DE(FA @(pPp`pp@` x  @   S" ,$@,  0H @ 0޽h ? fp=6.___PPT10.MP$+nD' 8= @B Dm' = @BA?%,( < +O%,( < +D' =%(%(DV' =%(D"' =4@BB"BB%()))D' =1:Bvisible*o3>+B#style.visibility<*@%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<*@%(D' d=+4 . B00B -1.0*[3>Bxshear<*@%(,))?)?D' d=0l9 BBBBBB*<3<*@%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<*@%(,))?)?D/' =A@BB"BB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*@%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<*@%(D' d=+4 . B00B -1.0*[3>Bxshear<*@%(,))?)?D' d=0l9 BBBBBB*<3<*@%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<*@%(,))?)?D"' =4@BB"BB%()))D' =1:Bvisible*o3>+B#style.visibility<*@%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<*@%(D' d=+4 . B00B -1.0*[3>Bxshear<*@%(,))?)?D' d=0l9 BBBBBB*<3<*@%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<*@%(,))?)?D/' =A@BB"BB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*@%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<*@%(D' d=+4 . B00B -1.0*[3>Bxshear<*@%(,))?)?D' d=0l9 BBBBBB*<3<*@%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<*@%(,))?)?D"' =4@BB"BB%()))D' =1:Bvisible*o3>+B#style.visibility<* @%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<* @%(D' d=+4 . B00B -1.0*[3>Bxshear<* @%(,))?)?D' d=0l9 BBBBBB*<3<* @%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<* @%(,))?)?D/' =A@BB"BB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*@%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<*@%(D' d=+4 . B00B -1.0*[3>Bxshear<*@%(,))?)?D' d=0l9 BBBBBB*<3<*@%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<*@%(,))?)?D"' =4@BB"BB%(X)))D' =1:Bvisible*o3>+B#style.visibility<* @%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<* @%(D' d=+4 . B00B -1.0*[3>Bxshear<* @%(,))?)?D' d=0l9 BBBBBB*<3<* @%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<* @%(,))?)?D/' =A@BB"BB0B%(X)))D' =1:Bvisible*o3>+B#style.visibility<*@%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<*@%(D' d=+4 . B00B -1.0*[3>Bxshear<*@%(,))?)?D' d=0l9 BBBBBB*<3<*@%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<*@%(,))?)?D"' =4@BB"BB%( )))D' =1:Bvisible*o3>+B#style.visibility<* @%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<* @%(D' d=+4 . B00B -1.0*[3>Bxshear<* @%(,))?)?D' d=0l9 BBBBBB*<3<* @%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<* @%(,))?)?D/' =A@BB"BB0B%( )))D' =1:Bvisible*o3>+B#style.visibility<*@%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<*@%(D' d=+4 . B00B -1.0*[3>Bxshear<*@%(,))?)?D' d=0l9 BBBBBB*<3<*@%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<*@%(,))?)?D"' =4@BB"BB%()))D' =1:Bvisible*o3>+B#style.visibility<* @%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<* @%(D' d=+4 . B00B -1.0*[3>Bxshear<* @%(,))?)?D' d=0l9 BBBBBB*<3<* @%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<* @%(,))?)?D/' =A@BB"BB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*@%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<*@%(D' d=+4 . B00B -1.0*[3>Bxshear<*@%(,))?)?D' d=0l9 BBBBBB*<3<*@%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<*@%(,))?)?D"' =4@BB"BB%()))D' =1:Bvisible*o3>+B#style.visibility<* @%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<* @%(D' d=+4 . B00B -1.0*[3>Bxshear<* @%(,))?)?D' d=0l9 BBBBBB*<3<* @%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<* @%(,))?)?D/' =A@BB"BB0B%()))D' =1:Bvisible*o3>+B#style.visibility<*@%(D ' ,=+4 . B(-#ppt_w/2)0B(#ppt_x)*Y3>B ppt_x<*@%(D' d=+4 . B00B -1.0*[3>Bxshear<*@%(,))?)?D' d=0l9 BBBBBB*<3<*@%(,))?)?D2' d=+4 )B-(#ppt_h/3+#ppt_w*0.1)*Y3>B ppt_x<*@%(,))?)?D-9' =%(D%' =A@BB4BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*@(%(D' =0l9 BBzCzCBB*<3<*@(%())?D' =.7 BBBBBM -0.46736 0.92887 C -0.37517 0.88508 -0.02552 0.75279 0.0908 0.66613 C 0.20747 0.57948 0.21649 0.50394 0.23177 0.40825 C 0.24705 0.31256 0.22118 0.15964 0.18264 0.09152 C 0.1441 0.02341 0.03802 0.0 0.0 0.0 *3>*B ppt_xB ppt_y=B0B<*@(%())?D' =-g6B fade*<3<*@(D%' =A@BB4BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*@(B%(D' =0l9 BBzCzCBB*<3<*@(B%())?D' =.7 BBBBBM -0.46736 0.92887 C -0.37517 0.88508 -0.02552 0.75279 0.0908 0.66613 C 0.20747 0.57948 0.21649 0.50394 0.23177 0.40825 C 0.24705 0.31256 0.22118 0.15964 0.18264 0.09152 C 0.1441 0.02341 0.03802 0.0 0.0 0.0 *3>*B ppt_xB ppt_y=B0B<*@(B%())?D' =-g6B fade*<3<*@(BD%' =A@BB4BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*@BF%(D' =0l9 BBzCzCBB*<3<*@BF%())?D' =.7 BBBBBM -0.46736 0.92887 C -0.37517 0.88508 -0.02552 0.75279 0.0908 0.66613 C 0.20747 0.57948 0.21649 0.50394 0.23177 0.40825 C 0.24705 0.31256 0.22118 0.15964 0.18264 0.09152 C 0.1441 0.02341 0.03802 0.0 0.0 0.0 *3>*B ppt_xB ppt_y=B0B<*@BF%())?D' =-g6B fade*<3<*@BFD' =4@BB4BB%(D' =1:Bvisible*o3>+B#style.visibility<*@%(D' =0l9 BBzCzCBB*<3<*@%())?D' =.7 BBBBBM -0.46736 0.92887 C -0.37517 0.88508 -0.02552 0.75279 0.0908 0.66613 C 0.20747 0.57948 0.21649 0.50394 0.23177 0.40825 C 0.24705 0.31256 0.22118 0.15964 0.18264 0.09152 C 0.1441 0.02341 0.03802 0.0 0.0 0.0 *3>*B ppt_xB ppt_y=B0B<*@%())?D' =-g6B fade*<3<*@D' =4@BB4BB%(D' =1:Bvisible*o3>+B#style.visibility<*@%(D' =0l9 BBzCzCBB*<3<*@%())?D' =.7 BBBBBM -0.46736 0.92887 C -0.37517 0.88508 -0.02552 0.75279 0.0908 0.66613 C 0.20747 0.57948 0.21649 0.50394 0.23177 0.40825 C 0.24705 0.31256 0.22118 0.15964 0.18264 0.09152 C 0.1441 0.02341 0.03802 0.0 0.0 0.0 *3>*B ppt_xB ppt_y=B0B<*@%())?D' =-g6B fade*<3<*@D' =4@BB4BB%(D' =1:Bvisible*o3>+B#style.visibility<*@%(D' =0l9 BBzCzCBB*<3<*@%())?D' =.7 BBBBBM -0.46736 0.92887 C -0.37517 0.88508 -0.02552 0.75279 0.0908 0.66613 C 0.20747 0.57948 0.21649 0.50394 0.23177 0.40825 C 0.24705 0.31256 0.22118 0.15964 0.18264 0.09152 C 0.1441 0.02341 0.03802 0.0 0.0 0.0 *3>*B ppt_xB ppt_y=B0B<*@%())?D' =-g6B fade*<3<*@D%' =A@BB4BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*@%(D' =0l9 BBzCzCBB*<3<*@%())?D' =.7 BBBBBM -0.46736 0.92887 C -0.37517 0.88508 -0.02552 0.75279 0.0908 0.66613 C 0.20747 0.57948 0.21649 0.50394 0.23177 0.40825 C 0.24705 0.31256 0.22118 0.15964 0.18264 0.09152 C 0.1441 0.02341 0.03802 0.0 0.0 0.0 *3>*B ppt_xB ppt_y=B0B<*@%())?D' =-g6B fade*<3<*@D' =4@BB4BB%(D' =1:Bvisible*o3>+B#style.visibility<*@%(D' =0l9 BBzCzCBB*<3<*@%())?D' =.7 BBBBBM -0.46736 0.92887 C -0.37517 0.88508 -0.02552 0.75279 0.0908 0.66613 C 0.20747 0.57948 0.21649 0.50394 0.23177 0.40825 C 0.24705 0.31256 0.22118 0.15964 0.18264 0.09152 C 0.1441 0.02341 0.03802 0.0 0.0 0.0 *3>*B ppt_xB ppt_y=B0B<*@%())?D' =-g6B fade*<3<*@D' =4@BBB B%(,D' =1:Bvisible*o3>+B#style.visibility<*@%(D' =+4 8?dCB0-#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*@D' =+4 8?dCB0-#ppt_h/2BCB#ppt_yB*Y3>B ppt_y<*@D' =A@BBB B0B%(,D' =1:Bvisible*o3>+B#style.visibility<*@%(D' =+4 8?dCB0-#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*@D' =+4 8?dCB0-#ppt_h/2BCB#ppt_yB*Y3>B ppt_y<*@+0+0+@0 ++0+@0 ++0+@0 ++0+@0 ++0+@0 ++0+@0 ++0+@0 ++0+@0 ++0+@0 ++0+@0 +   0 045D(  Dr D S 8p  8 |2 D T ZYI |2 D T ZYII|2 D T Z9YI|2 D T ZyYI|2 D T ZYI   D 0D   <Object( 2  D 0 - 7T( 2  D 0 m- 7U( 2  D 0 n 7V( 2  D 0T  7W( 2 D 0p     o.inv == "8 ( 2  D 0H  3o 2 D 3 BC DE(F @(pPp`pp@` x  @   S" Yy2 D  `? Z)  2 D  `? Z)  I2 D  `? Z9)  |2 D T Zy)  |2 D T Z)   D 0   <Object( 2 D 0! -  7T( 2 D 0% m - 7U( 2 D 0)  n 7V( 2 D 0-   7W( 2 D 0/  i  x o.inv == U8 ( 2  D 05   3o 2 D 3 BC DE(F @(pPp`pp@` x  @   S" YY I 2 D  `? Z 2 D  `? ZI2  D  `? Z92 !D  `? Zy2 "D  `? Z  #D 0; t  <Object( 2 $D 0@> -t 7T( 2 %D 04C mt- 7U( 2 &D 0LG tn 7V( 2 'D 0J t 7W( 2 (D 0N  I ]  *o.inv == W == typeof(o)H+( 2  $$ )D 0T  3o 2 *D 3 BC DE(F @(pPp`pp@` x  @   S" Y)RB +D s *Do y  RB ,D s *Do I RB -D s *Do  RB .D s *DoI RB /D s *DoII^B 0D 6D ^B 1D 6DI`` XB 2D 0D XB 3D 0D p x 4D c $[   0    5D 0T\ I P0  f" o is consistent ( 2 H D 0޽h ? fp=___PPT10i.Mx+D='  = @B +  0  p(  x  c $z      3 rx{ 0e0e #" 0e`   RB @ s *D@ P   00͒ P   d,invariant holds here (checked at call sites)- 2-V  0   . Tmeaning: ("t:T e t.inv <: T ! t.x < t.y).+ 2 &P RB  s *DH  0޽h ? fp=___PPT10i.M I+D='  = @B +  0 pTj(  Tr T S 4     T 3 r 0e0e #" 0e`   RB T@ s *D@ P  T 0  P   d,invariant holds here (checked at call sites)- 2-V T 0ؔ   . Tmeaning: ("t:T e t.inv <: T ! t.x < t.y).+ 2 &P RB T s *DH T 0޽h ? fp=___PPT10i.M I+D='  = @B + h  0 e*]*@?KH)(  Hr H S ȡ    |2 H T Z 9 |2 H T Z) y|2 H T Zi |2 H T Z |2 H T Z 9  H 0见    <Object( 2  H 0, ]  7T( 2  H 0 ] 7U( 2  H 0  7V( 2  H 0  7W( 2 H 0  `  no.inv == "$ ( 2   H 0D  3o 2 H 3 BC DE(F @(pPp`pp@` x  @   S" P@I2 H  `? Z 9 2 H  `? Z) y2 H  `? Zi |2 H T Z |2 H T Z 9 H 0Ł  {K  <Object( 2 H 0Ɂ ]{K   7T( 2 H 0(́ {K ] 7U( 2 H 0с {K  7V( 2 H 0ԁ {K  7W( 2 H 0(؁    d o.inv == U$ ( 2   H 0܁ p 3o 2 H 3 BC DE(F @(pPp`pp@` x  @   S" I2 H  `? Z p9 2 H  `? Z) py2  H  `? Zi p2 !H  `? Z p2 "H  `? Z p9 #H 0l  +  <Object( 2 $H 0 ]+   7T( 2 %H 0 + ] 7U( 2 &H 0l +  7V( 2 'H 0, +  7W( 2 (H 04  P  l o.inv == W, ( 2 $ )H 0  @  3o 2 *H 3 BC DE(F @(pPp`pp@` x  @   S"  I 4H 0D    D consistent ( 2 2 5H  `? Zp0 2 6H  `? Z pp2 7H  `? Z`p2 8H  `? Zp2 9H  `? Zp0 :H 0T  +  <Object( 2 ;H 0 T+  7T( 2 H 0, + 7W( 2 ?H 0  P  l o.inv == W, ( 2 $ @H 0T  @ 3o 2(2 BH C 33A.? ZDark downward diagonalS" ?p,$@ 0 AH 3 BC DE(F @(pPp`pp@` x  @   S" @r DH 6 " ,$@ 0r EH 6 P" ,$D 0 FH 0p   ,$ 0 Aexposed( 2 GH 0D$ C"? @ ,$ 0 ?owned( 2 HH 0@(  p  D consistent ( 2 t IH C +  P ,$ 0 Only consistent objects can be owned Special field exposed keeps track of exposed/owned exposed can be used in method specificationsXXP-$P3&" KH <4  p,$D, 0 9owned H H 0޽h ? fp=c=[=___PPT10;=.MP+yRD/<' 9 = @B D;' = @BA?%,( < +O%,( < +D!;' =%(%(D%' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*BH%(D' D=-s6Bwipe(down)*<3<*BH%(D' =eB]0,0; 0.14,0.36; 0.43,0.73; 0.71,0.91; 1.0,1.0+4 8?fCB#ppt_x-0.25BCB#ppt_xB*Y3>B ppt_x<*BH%(D' =mBe0.0,0.0; 0.25,0.07; 0.50,0.2; 0.75,0.467; 1.0,1.0+4 8?lCB?B'#ppt_y-sin(pi*$)/3CB?B*Y3>B ppt_y<*BH%(D' =B0, 0; 0.125,0.2665; 0.25,0.4; 0.375,0.465; 0.5,0.5; 0.625,0.535; 0.75,0.6; 0.875,0.7335; 1,1+4 8?lCBB'#ppt_y-sin(pi*$)/9CB?B*Y3>B ppt_y<*BH%(D' L=B0, 0; 0.125,0.2665; 0.25,0.4; 0.375,0.465; 0.5,0.5; 0.625,0.535; 0.75,0.6; 0.875,0.7335; 1,1+4 8?nCBB)#ppt_y-sin(pi*$)/27CB?B*Y3>B ppt_y<*BH%(,D' =B0, 0; 0.125,0.2665; 0.25,0.4; 0.375,0.465; 0.5,0.5; 0.625,0.535; 0.75,0.6; 0.875,0.7335; 1,1+4 8?nCBB)#ppt_y-sin(pi*$)/81CB?B*Y3>B ppt_y<*BH%(xD' =0l9 BBBpB*<3<*BH%(D' =0l9 BBBB*<3<*BH%())?D' =0l9 BBBB*<3<*BH%( D' =0l9 BBBB*<3<*BH%(:))?D' =0l9 BBBB*<3<*BH%(jD' =0l9 BBBB*<3<*BH%())?D' =0l9 BBBB*<3<*BH%(D' =0l9 BBBB*<3<*BH%(*))?D' =A@BBBB0B%(,D' =1:Bvisible*o3>+B#style.visibility<*KH%(D' D=-s6Bwipe(down)*<3<*KH%(D' =eB]0,0; 0.14,0.36; 0.43,0.73; 0.71,0.91; 1.0,1.0+4 8?fCB#ppt_x-0.25BCB#ppt_xB*Y3>B ppt_x<*KH%(D' =mBe0.0,0.0; 0.25,0.07; 0.50,0.2; 0.75,0.467; 1.0,1.0+4 8?lCB?B'#ppt_y-sin(pi*$)/3CB?B*Y3>B ppt_y<*KH%(D' =B0, 0; 0.125,0.2665; 0.25,0.4; 0.375,0.465; 0.5,0.5; 0.625,0.535; 0.75,0.6; 0.875,0.7335; 1,1+4 8?lCBB'#ppt_y-sin(pi*$)/9CB?B*Y3>B ppt_y<*KH%(D' L=B0, 0; 0.125,0.2665; 0.25,0.4; 0.375,0.465; 0.5,0.5; 0.625,0.535; 0.75,0.6; 0.875,0.7335; 1,1+4 8?nCBB)#ppt_y-sin(pi*$)/27CB?B*Y3>B ppt_y<*KH%(,D' =B0, 0; 0.125,0.2665; 0.25,0.4; 0.375,0.465; 0.5,0.5; 0.625,0.535; 0.75,0.6; 0.875,0.7335; 1,1+4 8?nCBB)#ppt_y-sin(pi*$)/81CB?B*Y3>B ppt_y<*KH%(xD' =0l9 BBBpB*<3<*KH%(D' =0l9 BBBB*<3<*KH%())?D' =0l9 BBBB*<3<*KH%( D' =0l9 BBBB*<3<*KH%(:))?D' =0l9 BBBB*<3<*KH%(jD' =0l9 BBBB*<3<*KH%())?D' =0l9 BBBB*<3<*KH%(D' =0l9 BBBB*<3<*KH%(*))?D' =%(Dp' =A@BB*BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*GH%(D' =-g6B fade*<3<*GHD' =+4 8?\CB#ppt_xBCB#ppt_xB*Y3>B ppt_x<*GHD' =+4 8?bCB#ppt_y+.1BCB#ppt_yB*Y3>B ppt_y<*GHDc' =4@BB*BB%(D' =1:Bvisible*o3>+B#style.visibility<*DH%(D' =-g6B fade*<3<*DHD' =+4 8?\CB#ppt_xBCB#ppt_xB*Y3>B ppt_x<*DHD' =+4 8?bCB#ppt_y+.1BCB#ppt_yB*Y3>B ppt_y<*DHDp' =A@BB*BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*FH%(D' =-g6B fade*<3<*FHD' =+4 8?\CB#ppt_xBCB#ppt_xB*Y3>B ppt_x<*FHD' =+4 8?bCB#ppt_y+.1BCB#ppt_yB*Y3>B ppt_y<*FHDc' =4@BB*BB%(D' =1:Bvisible*o3>+B#style.visibility<*EH%(D' =-g6B fade*<3<*EHD' =+4 8?\CB#ppt_xBCB#ppt_xB*Y3>B ppt_x<*EHD' =+4 8?bCB#ppt_y+.1BCB#ppt_yB*Y3>B ppt_y<*EHD' =%(D8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*IH%(D' =-g6B fade*<3<*IH++0+FH0 ++0+GH0 ++0+IH0 ++0+KH0 +A  0L0 p0(  p2 p  ff? c Z<"`` @ 2 p  ff? c Z<"`@ 2 p # l? c Z<"`@ P  p C xPp ? p  5p  p C xt ?``  5q  p C xy ?@00  >    p 0T| < jz  7U( 2  p 0$  p  7T( 2  p 0  P <Object( 22  p NZpA,$@ 02 p NZA0,$@ 0 p 0  ,$ 0 <Object( 2 p 0  ,$  0 7Q( 22 p NZ ,$@  02 p NZ`,$@  02 p NZ ,$@  0 p 0\ D ,$  0 <Object( 2 p 0 ~,$ 0 7P( 2 p 0 ,$ 0 7R( 2$ p 3 BC0DE4F 0\48`(x`h0px` @    @@,$@ 0$ p 3 BpCXDE4F XP(pH xp 8|p @     ,$@ 0 p 0$ A( ,$ 0 :26 2 p 0ܡ 0P9  5x 22 p  ff? c Z<"`p@ 2 p  ff? c Z<"` @  p 0 p,  7V( 2 p 0쩓 p 7W( 2x  p c $    H p 0޽h ? fp=++___PPT10+.Mj+AD)'  = @B DX)' = @BA?%,( < +O%,( < +D(' =%(%(D ' =%(D' =A@BBBB0B%()?)D' =.7 BBBBBM 0.0 0.0 C 0.00625 -0.09711 0.0125 -0.19445 0.00834 -0.29966 C 0.00417 -0.40509 -0.01041 -0.51885 -0.025 -0.6326 *3>*B ppt_xB ppt_y=0BB aaA<*pD' =A@BBBB0B%()?)D' =.7 BBBBBM 0.0 0.0 C 0.00625 -0.09711 0.0125 -0.19445 0.00834 -0.29966 C 0.00417 -0.40509 -0.01041 -0.51885 -0.025 -0.6326 *3>*B ppt_xB ppt_y=0BB aaA<*pD' =4@BBBB%()?)D' =.7 BBBBBM 0.0 0.0 C 0.00625 -0.09711 0.0125 -0.19445 0.00834 -0.29966 C 0.00417 -0.40509 -0.01041 -0.51885 -0.025 -0.6326 *3>*B ppt_xB ppt_y=0BB aaA<*pD' =4@BBBB%()?)D' =.7 BBBBBM 0.0 0.0 C 0.00625 -0.09711 0.0125 -0.19445 0.00834 -0.29966 C 0.00417 -0.40509 -0.01041 -0.51885 -0.025 -0.6326 *3>*B ppt_xB ppt_y=0BB aaA<*pD5' =%(D+' =4@BB BB%(D' =1:Bvisible*o3>+B#style.visibility<* p%(D' =-g6B fade*<3<* pD+' =4@BB BB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =-g6B fade*<3<*pD8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =-g6B fade*<3<*pD8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =-g6B fade*<3<*pD+' =4@BB BB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =-g6B fade*<3<*pD+' =4@BB BB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =-g6B fade*<3<*pD+' =4@BB BB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =-g6B fade*<3<*pD8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =-g6B fade*<3<*pD8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =-g6B fade*<3<*pD8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =-g6B fade*<3<*pD+' =4@BB BB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =-g6B fade*<3<*pD+' =4@BB BB%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =-g6B fade*<3<*pD8' =A@BB BB0B%(D' =1:Bvisible*o3>+B#style.visibility<*p%(D' =-g6B fade*<3<*p++0+p0 ++0+p0 ++0+p0 ++0+p0 ++0+p0 ++0+p0 ++0+p0 ++0+p0 +y  0 #l (  l2 l  ff? c Z<"`` @ 2 l  ff? c Z<"`@ x l c $P͓     2 l # l? c Z<"`@ P  l C x`ϓ ? p  5p  l C xӓ ?``  5q  l C xؓ ?@00  >    l 0dۓ < jz  7U( 2  l 04ߓ  p  7T( 2  l 0(  P <Object( 2x l c $    v2 l NZpAv2 l NZA0 l 0   <Object( 2 l 0   7Q( 2v2 l NZ v2 l NZ`v2 l NZ  l 0x D  <Object( 2 l 0 ~ 7P( 2 l 0  7R( 2 l # BC0DE4FAA 0\48`(x`h0px` @    @@ l # BpCXDE4FAA XP(pH xp 8|p @      l 0T A(  :26 2 l 0 0P9  5x 2  l # BC DE(FAA p 0@(8`  @   000 !l # BCDE(FAA TH`0 P @   0  "l # BCDE(FAA $0H `xxP @   P@ @H l 0޽h ? fp=___PPT10i.Mj+D='  = @B +I-  0 #$x(  x2 x  ff?  Z<"`` @ 2 x  ff?  Z<"`@ 2 x # l? c Z<"`@ P 2 x # l?  Z<"`@ P ,$D  0x x c $\  0    x C x  ? p  5p  x C xP ?``  5q  x C x ?@00  >    x 0  p  7T( 2  x 0#  P <Object( 2x  x c $&    2  x Z?ZpA2 x Z?ZA0 x 0(   <Object( 2 x 0-   7Q( 22 x Z?Z 2 x Z?Z`2 x Z?Z  x 01 D  <Object( 2 x 05 ~ 7P( 2 x 09  7R( 2 x 3 BC0DE4F 0\48`(x`h0px` @    @@ x 0= A(  :26 2 x 0A 0P9  5x 2 x 3 BCDE(F TH`0 P @   0  x 3 BCDE(F $0H `xxP @   P@ @  x 0E < jz  7U( 2(2  x C 33A.? ZDark downward diagonalS" ? n ,$D 0dB "x <Do@PP  #x 0J P ,$ 0 V o.inv == U 2  $x 04 P  V o.inv == T 2  x 3 BpCXDE4F XP(pH xp 8|p @      x 3 BC DE(F p 0@(8`  @   000" !x <4R @q,$D  0 9owned H x 0޽h ? fp=___PPT10.Mj+8LD' V = @B D' = @BA?%,( < +O%,( < +D' =%(D' =%(D' =4@BB5BB@%()))D' =1:Bvisible*o3>+B#style.visibility<* x%(D' =+4 8?RCBBCB#ppt_wB*Y3>B ppt_w<* xD' =+4 8?RCBBCB#ppt_hB*Y3>B ppt_h<* xD' =-g6B fade*<3<* xD' =%(D' =4@BBBB@%()?)?D' =.7 BBBBBM 0.0 0.0 C 0.09114 -0.09805 0.18229 -0.19611 0.21632 -0.21669 C 0.25035 -0.23728 0.18229 -0.11332 0.20434 -0.12326 C 0.22639 -0.1332 0.31597 -0.26248 0.34913 -0.27636 C 0.38229 -0.29024 0.39253 -0.24861 0.40295 -0.20675 *3>*B ppt_xB ppt_y=0BB aaaaA<* xD' =%( DD' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*!x%(D' =-s6Bwipe(left)*<3<*!xD' =%( D7' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*x%(D' =-s6Bwipe(down)*<3<*xD' =%( D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*#x%(D' =A@BBBB0B%(D' =1:Bhidden*o3>+B#style.visibility<*$x%(++0+#x0 ++0+$x0 ++0+!x0 +U-  0 e]##|(  |2 |  ff?  Z<"`` @ 2 |  ff?  Z<"`@ 2 | # l? c Z<"`@ P 2 | # l?  Z<"`@ P x | c $l  p    | C xm ? p  5p  | C x,q ?``  5q   | C xv ?@00  >    | 0Lu  p  7T( 2  | 0|  P <Object( 2x  | c $~    2  | Z?ZpA2 | Z?ZA0 | 0܁   <Object( 2 | 0   7Q( 22 | Z?Z 2 | Z?Z`2 | Z?Z  | 0̊ D  <Object( 2 | 0 ~ 7P( 2 | 04  7R( 2 | 3 BC0DE4F 0\48`(x`h0px` @    @@ | 0L A(  :26 2 | 0 0P9  5x 2 | 3 BCDE(F TH`0 P @   0  | 3 BCDE(F $0H `xxP @   P@ @ | 0Ȝ < jz  7U( 22 | C 33A.? ZDark downward diagonalS" ?ppB !| HDo@PP  "| 0, P  V o.inv == U 2  #| 0L P ,$ 0 V o.inv == T 2  | 3 BpCXDE4F XP(pH xp 8|p @      | 3 BC DE(F p 0@(8`  @   000"  | < @q 9owned H | 0޽h ? fp=___PPT10p.Mj+OD'  = @B DW' = @BA?%,( < +O%,( < +D' =%(D' =%(Da' =4@BBBB%()))D' =-o6Bwipe(up)*<3<*|D' =1:Bhidden*o3>+B#style.visibility<*|%(D' =%(D' =A@BBBB0B%())))?D' =1:Bhidden*o3>+B#style.visibility<*"|%(D' =A@BBBB0B%())))?D' =1:Bvisible*o3>+B#style.visibility<*#|%(D' =%(Dt' =A@BBBB0B%()))D' =-u6Bwipe(right)*<3<* |D' =1:Bhidden*o3>+B#style.visibility<* |%(D' =%(D' =4@BBBB@%()?)?D' =.7 BBBBBM -4.16667E-6 -3.33333E-6 C -0.00885 -0.0368 -0.01753 -0.07338 -0.04861 -0.0588 C -0.07968 -0.04421 -0.16527 0.07801 -0.1868 0.0882 C -0.20833 0.09838 -0.1434 -0.01852 -0.17795 0.00208 C -0.2125 0.02269 -0.30329 0.11713 -0.39409 0.21181 *3>*B ppt_xB ppt_y=0BB aaaaA<*|D' =4@BB5BB@%()))D' =+4 8?PCB ppt_wBCBB*Y3>B ppt_w<*|D' =+4 8?PCB ppt_hBCBB*Y3>B ppt_h<*|D' =-g6B fade*<3<*|D' =1:Bhidden*o3>+B#style.visibility<*|%(++0+"|0 ++0+#|0 ++0+ |0 +  0 #)h{(  h2 h  `?Z r h S HI1x`   2 h  ff? c Z<"`` @ 2 h  ff? c Z<"`@ 2 h # l? c Z<"`@ P  h C x ? p  5p  h C xŖ ?``  5q   h C xLʖ ?@00  >    h 0̖ < jz  7U( 2  h 0Ж  p  7T( 2  h 0Ԗ  P <Object( 2  h 0Hؖ A(  :26 2 h 0@ܖ 0P9  5x 2v2 h NZpA2 h  `Y?Z"`A0 h 0|   <Object( 2 h 0P   7Q( 2|2 h T?Z 2 h  `?Z` h 0 D  <Object( 2 h 0ږ ~ 7P( 2 h 0  7R( 2 h 3 BC0DE4F 0\48`(x`h0px` @    @@ h 3 BpCXDE4F XP(pH xp 8|p @      h 3 BC DE(F p 0@(8`  @   000 h 3 BCDE(F TH`0 P @   0  h 3 BCDE(F $0H `xxP @   P@ @4  h 0 B p <  class U { & invariant x d" p.g '" p.g == p.h; invariant x d" q.k;B 2b  # "  #  P XB "h 0D)0  XB #h 0D)0   $h S ~ ?|4T 3h  &h S ~ ?|0P 3k  %h S ~D ?|` 3g  'h C   @  rBFields of owned (un-exposed) objects are not allowed to be mutatedCCH h 0޽h ? fp=___PPT10i.MPR`+D=' U= @B +  0 X-(  XX X 0p  r X S "    r X S "       X 6h$  x1  ;new 2 H X 0޽h ? fp=___PPT10i.M]+D=' U= @B +E  0 \T@'(  2   `?Z x  c $3 x   2   ff?  Z<"`` @ 2   ff?  Z<"`@ 2  # l?  Z<"`@ P   C x\8 ? p  5p    C x= ?@00  >     0|< < jz  7U( 2   0D  p  7T( 2   0H  P <Object( 2   0K A(  :26 2  0O 0P9  5x 2|2  T?Z 2   `?Z`  0R D  <Object( 2  0V ~ 7P( 2  0DZ  7R( 2  3 BpCXDE4F XP(pH xp 8|p @       3 BC DE(F p 0@(8`  @   000  0_ B p   bZclass U { & invariant x d" p.g '" p.g == p.h;. 2b  # " >    S ~db ?|4T 3h  " S ~v ?|` 3g 2 $ C 33A.? ZDark downward diagonalS" ?p" % <,y @q 9owned  & 0}  5o 2 ' 3 BC DE(F @(pPp`pp@` x  @   S" u:H  0޽h ? fp=___PPT10i.MPR`+D=' U= @B +}  0 \$(  \r \ S  0@(   r \ S  @0    H \ 0޽h ? fp=___PPT10i.Mz+D=' U= @B +  0 `J(  `r ` S @ 0   r ` S 腙 `    2 ` # l?x c Z<"`P & ` C x ? ?exposed  ` C x0 ?.p| ;inv  ` 0  :Object( 2H ` 0޽h ? fp=___PPT10i.M/+D=' U= @B +r`@}Y%<Z0e,@P!0X@Dqz 7 wOh+'0 hp  $ 0 <HP<Verification of object-oriented programs with invariantsRustan LeinoCrayonsRustan Leino32Microsoft Office PowerPoint@]@`@ G@0RGHg  `  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-. 2 /Verification of."System7-2HGPSoeiKakupoptai-. 2 9object.-2HGPSoeiKakupoptai-.  2 97-.-2HGPSoeiKakupoptai-. !2 9=oriented programs.-2HGPSoeiKakupoptai-. 2 D(with invariants.-2HGPSoeiKakupoptai-. 2 0Verification of.. 2 /Verification of.-2HGPSoeiKakupoptai-. 2 :object.. 2 9object.-2HGPSoeiKakupoptai-.  2 :7-..  2 96-.-2HGPSoeiKakupoptai-. !2 :=oriented programs.. !2 9<oriented programs.-2HGPSoeiKakupoptai-. 2 E(with invariants.. 2 D'with invariants.-2HGPSoeiKakupoptai-. 2 J< Mike Barnett,t.. 2 I; Mike Barnett,t.-2HGPSoeiKakupoptai-. 2 O?Robert DeLine,.. 2 N>Robert DeLine,.-2HGPSoeiKakupoptai-. 2 SCManuel .. 2 RBManuel .-2HGPSoeiKakupoptai-. 2 SQ FahndrichL.. 2 RP FahndrichL.-2HGPSoeiKakupoptai-.  2 Sc,..  2 Rb,.-2HGPSoeiKakupoptai-. $2 WGK. Rustan M. Leino,.. p=$2 VFK. Rustan M. Leino,.-2HGPSoeiKakupoptai-. 2 \KWolfram Schulte.. 2 [JWolfram Schulte.-2HGPSoeiKakupoptai-. .2 hFormal techniques for Java.-2HGPSoeiKakupoptai-.  2 h6-.-2HGPSoeiKakupoptai-. 2 h9 like programs.-2HGPSoeiKakupoptai-. "2 lDarmstadt, Germany.-2HGPSoeiKakupoptai-. 2 q 21 July 2003.-2HGPSoeiKakupoptai-.  2 TSN.-՜.+,0     On-screen ShowMicrosoft Corporation HGPSoeiKakupoptaiArialArial Unicode MSCrayonsEVerification of object-oriented programs with invariantsExample problem#Wanted: Methodology for invariants)Invariant declarations one per subclass7Special field inv keeps track of which invariants hold)inv can be used in method specifications)inv can be used in method specificationsExposed vs. owned Components Components Components Components4Fields of components can be mentioned in invariantsLicense to modify5Method calls may change fields of un-exposed objects Related work Conclusions  Fonts UsedDesign Template Slide Titles$_ 0Rustan LeinoRustan Leino  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuwxyz{|}~Root EntrydO)PicturesCurrent UserSummaryInformation(vPowerPoint Document(DocumentSummaryInformation8