ࡱ> t(@ / 0DArialiKakupopta``/=T0DArial Unicode MS`/=T0" DCalibriicode MS`/=T0"0DSymbolicode MS`/=T0@DTimes New Roman`/=T0PDArial Narrowan`/=T0"`DHGPSoeiKakupoptai`/=T02 B . @n?" dd@  @@`` 8-  X[      lop r-u vD1H       &1H#1 *"    OS V3      )/ ;,,+1 0 3f3@ʚ;ʚ;<4dddd,#0,g4{d{dTr=T0ppp@  <42d2d,O$0`E)___PPT12 %0___PPT10 ``___PPT9{.4 .2?  O  ]PjFLecture 3 Towards a Verifying Compiler: Verifying Object InvariantsG G$ G R Wolfram Schulte Microsoft Research Formal Methods 2006 Program Invariants, Callbacks, Aggregates, Ownership, Visibility _____________ Joint work with Rustan Leino, Mike Barnett, Manuel Fhndrich, Herman Venter, Rob DeLine, Wolfram Schulte (all MSR), and Peter Mller (ETH), Bart Jacobs (KU Leuven) and Bor-Yuh Evan Chung (Berkley) {    C "C "  , Z     Q   f#Review: Verification of OO Programs$$$ $ cWhat is needed for designing a verifier? Which programs can we verify? What are the limitations? >) :( : d S.&Pre- and Postconditions are not Enough' '$ ' Contracts can break abstraction class C{ private int a, z; public void M() requires a!=0; {z = 100/a;} }  ! P  Pa " P P  &9  Q  yWe need invariants class C{ private int a, z; invariant a!=0; public void M() {z = 100/a;} }  Z  ZZ " Z ZZ3f &+  L J0Dealing with Invariants  ^Basic Methodology Object-based Ownership Object-oriented Ownership Visibility based Ownership  _3M _ `}Problem: Reentrancy    V How can we prevent that current object is re-entered in an inconsistent state? JVZZO W r#Program Model for Object Invariants$$$ $ xObjects can be valid or mutable inv { valid, mutable } is a new ghost field in each object Mutable objects need not satisfy their invariants o.inv indicates whether the invariant of o, Inv(o), is allowed to be broken "o: o.inv mutable Inv(o) Remark: Quantifier ranges over allocated, non-null objects P > ">"" 3f3f3f3f9O 3f3f3f3f3f 3f3f 3f3f 3f?t  '  !     C  Field Updates  Only fields of mutable objects can be updated Tr[[o.f = e]] = assert onull '" o.inv=mutable; o.f := e 1<1 3f t1          bPack and Unpack  }inv is changed by special source commands unpack(o) to make o mutable pack(o) to re-establish invariant and make o valid +P+3f3f.@+    0 Pack and Unpack Example  Bvoid Reschedule( int d ) requires inv==valid 0d<7; { unpack(this); day = d; if ( day==6 ) time = 1200; pack(this); }  3f 3f  3fZ  0   A     Program Invariant  rTheorem (Soundness) "o: o.inv mutable Inv( o ) Admissible invariants contain only field accesses of the form this.f Proof sketch new: new object is initially mutable o.f := E; can only affect invariant of o, asserts o.inv = mutable unpack(o): changes o.inv to mutable pack(o): asserts Inv(o)Z*ZZFZZ ZZ Z Z8Z ZZ ZZ  F  8 "  V  6  0               K1Dealing with Invariants  ^Basic Methodology Object-based Ownership Object-oriented Ownership Visibility based Ownership (_36 _ cProblem: Object Structures  Can we have relax the admissabilty condition? How can we find out that reschedule might break Person s invariant?rr&   P |d(Invariants in the Presence of Aliasing? ))$ ) Ownership-Based Invariants  Establish hierarchy (ownership) on objects Ownership rule: When an object is mutable, so are its (transitive) owners An object o may only depend on the fields of o and the fields of objects (transitively) owned by o,JZZ ZDZ 3f3f:3f D    eDynamic Ownership  Each object has a special ghost field, owner, that points to its owner object rep(resentation) declarations lead to implicit owner invariants inv{committed, valid, mutable} An object is committed, if its invariant is known to hold the owner is not mutable 9'3f#3f#3f39@O  3  i gPack and Unpack with Ownership  Tr[[unpack o]] = assert o.inv = valid; o.inv := mutable; foreach (c c.owner = o) { c.inv := valid; }oZ' 3f3f#3f                 fTr[[ pack o]] = assert o.inv = mutable; assert "c: c.owner = o c.inv = valid; foreach (c c.owner = o) { c.inv := committed; } assert Inv( o ); o.inv := valid  3f3f3f3f 3f3f(3f3f3f                '     Program Invariant with Ownership ! Theorem (Soundness) "o: o.inv mutable Inv(o) ("c: c.owner = o c.inv = committed)) Admissible invariants contain only field accesses of the form this.f1. & .fn where f1 & .fn-1 must be rep fields *3f3f$3f> t         Method Framing Revisited  Allow methods to modify also committed objects Example. Given class A{ rep B b;} class B{ rep C c;} the method static void m(A a) requires a.inv == valid; modifies a.*; is allowed to modify & the fields of a.b and a.b.c|0'33 3  1t~     J     Method Framing Revisited  Allow methods to modify also committed objects The Post condition for a Spec# modifies W clause Tr [[W]] = ("o : ref, f: field :: old(Heap[o,allocated]) (o,f) old(W) old(Heap[o,f]) = Heap[o,f]) old(Heap[o,inv]) = committed X) 33 33  4  3$$3 ((3((a  !               hExample Revisited  L2Dealing with Invariants  ^Basic Methodology Object-based Ownership Object-oriented Ownership Visibility based Ownership (_)3 _ w Inheritance  eEach subtype defines one frame with its variables Single inheritance results in a sequence of frames *f3F  f }eRefined Representation      Refined Representation  N4Refined Representation  rep fields f in class T give rise to implicit invariants invariant this.f!= null let (p,T ) = this.f.owner in p== this '" T = T 9J 9  $ ZD         Pack and Unpack with Inheritance ! Tr[[unpack(o from T)]] = assert o.inv = T; assert !o.committed; o.inv := S foreach (c c.owner==(o,T)) { c.committed := false } F0 ZJZ 3 .                      nTr[[ pack o as T]] = assert o.inv = S; assert InvT( o ); assert "c: c.owner==(o,T) c.inv = typeof(r); foreach (c c.owner==(o,T)) { c.committed := true } o.inv := T   1 38                             Inheritance Precondition Problem ! |"Dynamic Dispatch and Preconditions##$ # `For virtual methods m, we allow to write the pre: this.inv == 1 For each frame in which m is defined we generate 2 procs m.C is used for statically bound calls; its pre: Heap[o,inv] = C m.C.Virtual is used for dynamically dispatched calls, its pre: Heap[o,inv] = typeof(o)2&93+?33 3313337 3 3<I  :    K      O       Inheritance Precondition Example !  M3Dealing with Invariants  ^Basic Methodology Object-based Ownership Object-oriented Ownership Visibility based Ownership ,_)3 _ hRep & Peer Objects  gRep fields are used to build hierarchical abstractions. Peer fields are used to group sibling objects.bh   3f 3 h iRep and Peer Objects  6class List { rep Node! head; invariant (" Node n | n.owner=this next!=null next.prev = this & } class Node{ peer Node next, prev; }   #  Z7     .    class List { rep Node! head; } class Node{ peer Node next, prev; invariant next!=null next.prev = this & } | @>       j$Mutually Recursive Object Structures % <Objects are mutually dependent Objects cannot own each other = k%Admissible Visibility-Based Invariant &  The invariant declared in class C may contain a field access R.f iff R is  this or R is  this.g1. & .gn. and g1..gn are rep or peer fields, and C is mentioned in the dependent clause of fHZyZH ,3Z?    "  V l"Proof Obligation for Field Updates # 0 For a field update o.f := E; we have to prove That o is non-null and mutable (as before) That all other objects whose invariant depends on o.f are mutable Tr[[o.spouse := E; ]] assert o null o.inv = mutable; assert "Person t: t.spouse = o t.inv = mutable; The other objects are determined by inspecting the invariants of the all  friend classes mentioned in the dependent clause (see next slide)@.nZX.n  $3. 3f  u            m.Marriage is Never Easy&   nSummary: Object Invariants  9The methodology solves the problems of Re-entrance (through the explicit inv field) Object structures (through ownership or visibility) It can handle Complex object structures including (mutual) recursion Ownership transfer (not shown in this talk) The methodology is modular and sound Aliasing is not restricted`'bc@'bc@ : /s#h 0` 33` Sf3f` 33g` f` www3PP` ZXdbmo` \ғ3y`Ӣ` 3f3ff` 3f3FKf` hk]wwwfܹ` ff>>\`Y{ff` R>&- {p_/̴>?" dd(3fx?" dd  " @ ` n?" dd@   @@``@n?" dd@  @@``PR    @ ` `p>>aN0 og  (     T<=?Rectangle 3073" `} = X Click to edit Master title style!! F  N=?Rectangle 3074" ` = RClick to edit Master text styles Second level Third level Fourth level Fifth level!    S   N4=?Rectangle 3075"^ ` = X F     Nļ=?Rectangle 3076"^  = n* C   Q   N=?Rectangle 1029#"A5PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!$K drs/shapexml.xmlVn6}/Zx-ɗ* ;m70eH'EgHIE~G&9sf̡>92 c+2|Y$TJ33bu\\j%24r/m"Uvdl\3vm5t#Jmjh+qjMxuk^)v gjln0QULk9@8n32ֶ* DajPjbj~^X\Bl"ݮF՞3' C>ܼdm}zSwN*|r(M}~NIeҳ v08(dž4!ǎ0tB;cW?WD2fZ-ϭJVR_T;36rQARrn@Y,rQʝY>8{&sZVE~]$ꌍbt7hy0bע`Ax%d'J+wY堎1p.( uЈsFlyFJniP P~u?H`^^pUƨgneXtOЙqS ^&4فjf^`Jse-!"-v*Ggm(Eu3fuZw()Ӝ]IA8$Vy_J(. %'Z^ia'H GKhGq N6w3n:m^\$_i{IV5IraЕjWIȘPopB^EH3Rz-mtG'YidE5~ma.&TA(O}7>Q GE5UۈPk;E"&I8Si*pПt=/ jfr|{/PK!Bn" drs/downrev.xmlD]K0CdZ!ls]޾6&I xy8<3_Z4unD NND΃PhC9$t:(0K}Pr Ԩw6VTX[Ut،TAÄ_%c8Ig4>xv}]6yxsoaZU ˆ_&AeKh9a.~PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!$K drs/shapexml.xmlPK-!Bn" drs/downrev.xmlPK*^ ` = r*  G   H  0޽h ? 3380___PPT10..fRPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!ۘݺ !drs/slideLayouts/slideLayout1.xmlVn0?'z!EiKuDB(JhΒ)椋M.})N覨  Uys,Xcʹ{.?광 ?T[Ͻ1uM%oΫZ(*]rOs~S䗼P^߃PVE&Vٶ8-$7puӡAhcw&e56cP0z x-e/1@l)\إ~B}v^"'v T0}!tbS$;/6T dv6wofooX` kџD;  {)֛*{n'nwLgF۰n݆ذv\`LID(Gq8E'A,Nvuj_@Q}?F^UlGxx 'Kɩ~:{\J33ya.Pf`E/pCu!]?C}r: qUt#d$SKAP*f'YStZ]zt )Jol*G!k\v1+ڬX |]Hi?BWRfOw*q3$Yۏ'8ǰG8FGILAbK$[#ߋpl jx|dw|g˖p%BGXGQIJ%ǣl 'GvEG,['ض0WuΉǺ96t{CzUڦ-^l$S S5az4+(] PK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!ۘݺ !drs/slideLayouts/slideLayout1.xmlPKs oPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!%խ</!drs/slideLayouts/slideLayout1.xml]o '? [c&+Ieko%9%~/8N6\i7y]oEZ4zNW#J榔z=ϫtɔbN׋/3{Uޱ s6u62k0eXkXЭұ?nT6eӬaRӽ`JrM#tdP,fI'voJRk1BD+ DFhoWN[g ҾYF~aiNnWbrbr 9ŵbM,@x7ɏ~<_'dp8Wn;GLz;Eͬ ル.aᯞh~g?XmM:!uG4 E/ ji;%8`9AHb }\ăXK%+ Rr|T@e6WTBi9A7[Tx0*ITE4/%%=rzՁQ,ޖV/:=:{4nH~4G/DI4c4qoD9C7] I:?2|Yd-m4vf7)x%cc\>PI )g;] bp)[Nd9"t@$); YLe?B3' /hu@υL?P-vt{WIû򜌣a?+yDQ#Uv0FɔDI&RW),$wʍSЌ EGD\!Y>1laHRw&IvM;O&~uDop-iQW2yDHiïKn*/fceFsY/ԙed?*'L͒3 "1$6Ǚ8ډhl'OHܐk Sإ@eo Ʃ A,˯ڤnZձ#JAS>Ur;~2'i[-vN$ZbS)uz%Sn »ph'2xnS6ͰtP_`u`;:[b=سC{~usDƸ 3clvDpV1~;VgYtI_R>+Ĩ>h{?Vwͺguʳ1ugz[wlƒYx*Qxܽi/R5-o+w9uwyzPK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!MQ~ !drs/slideLayouts/slideLayout1.xmlPKZPPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!LV!drs/slideLayouts/slideLayout1.xmlXr6*}F,KS'cOEHd$|t7ZCхȇ^m[ U8D8-^'㧱*͋gΗ鯿ܗaO]4 I.^,EߖR\OڋG ~ƽymg/V>ՙq#+)Ko~;:_5*=d:s)mkEvESv$U޵hчR\( E`5G_$\XĤ[Շ+.R K8ٲ-#)x:R,p>0ݲ幣`<-nB B"i'٪ao`hţ\X2 k%%hX[m,kۉڊZ`mub-v:XS@(6gC=/mH[YMbw r1ٙюEk k4ڻ&SδS&_7θ|__̓x&F.JxRBDUi qv+=ZHtč(q;ދ;av|pK|YJ?{ڥ jĪqt ԑlzPi(YOĆ)Z9< *׼aXf.:bh F8oF'm6G`miYK"MLAuDU:RL=4?NPK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!"G~!drs/slideLayouts/slideLayout1.xmlPKPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!%,% N !drs/slideLayouts/slideLayout1.xmlWݎ8_i} ! 0@LU>I$[ǎ}=c&2J{s|;';RELx\>TKi;zOB4)]u:5Y*ڼ5x(W+>Q4h)A am2{ЎF1N5hn<[=V]7Jj8,7<bj0Xls"hG bA1fbe(R憪Ff 0?z&Z1!Ehdn2{͊gY z7My;κ5#+Xz' ~{Γ }]~]jZ{i񍍩78l8&hb(b"IzTDt_$NiFڍ 9oZ82NS!l#?8ꁦ9~T"u0ocp#wxl"$x`)-xm/DKROL5-1҂c"+ ]>Uչl9{aV5?C68!'MIc/^ Whyg.DTs /BPK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!%,% N !drs/slideLayouts/slideLayout1.xmlPKUPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!M/"N!drs/slideLayouts/slideLayout1.xmlXr6}L׎#Swk,gbn38- ,{v td/,g/]464>qJ4~{6^ k9 u~bbj& DLõsŤӱZf~ &桳2 Йtχ^'=9!O4&ڕ0F*᠀]Њc #-`xs4߅ -& 01Oc12xJ:݄elqo$ibnxvntEP"/Ưbt?THbKLvu)&I3=ILq9׳+W;P(5Qnb- D{JQ<~Ρ'_m+0ҙuPߥNI/W.=*y6.D4vǠ.4 af0zc>B!%t1q|L&]3N-tA%me=+㭊p@!d%o/{yk l*Aq)EyQi<_ul6..Ca1]+J[{mv`@崓܊ gEӜ;Ѡ4EoQD &\Bđ0x2,la>k; /~sx1͕ekG8p. fzQ^+d̘f^!Iѐx!3Q^Kd1 K(/.| ^xq,[xQoQwA= xAp,p xa tCBϞ;AeB8 ^4щN!fbVÖ 79q} @{\ uE y3}my}⤻]kdPt (Is[[֐ɡ,e%>%Hm܆_]nnqD/7_Arf]# Γz5FPydimT@%PP{a2LF 4b)%z)J_ߩEůduRks Y:M36W&X>JQ%&Bkk$qfZ I&]eL{cn(?fzp-gQbA%(b{[ju\lb#[loS:k_ws/1JM)Tu>U+jS5e*{l9Z 鸦-L IFrCɡPVyN,]@FTZh-χ4/PK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!M/"N!drs/slideLayouts/slideLayout1.xmlPKvnPK!M[Content_Types].xml|N0 EHC-jaj; +,Kq:=ig ,?ϵYD&oDzCwO-gkcg$./XQ{jsԈHt䒦AFP0skfx(壓8?.C(ũ{R(Mb˳7{-IF#{_R'dK0FFjr'"&@_'PK!p8ܾ8 _rels/.rels 0Dnz x%ٶ6 (тqLݾQ(NAU ioo'tGHL m^W16 AJMȅ8a22~`Or[;,lij@搛}YMGBh ]pϔ{J Loc!"rPK!};7!drs/slideLayouts/slideLayout1.xmlݎ +OUUVv{@1b@@\{vM# 101aq֊4yiN'M)nI7W_()ŒjCoV?,lUyf$ْV!<,M59Xn]Z(HCq(nVyx&WDgCTpL붝vfbVUpOhA,z"=6!ރiگ,&j F|vj,&F; U4NW%D5'O06eL1 YTnSjb|YqSI7^p5%fB5O#>LؽDOV5}lRxd,c)-_PK-!M[Content_Types].xmlPK-!p8ܾ8 ._rels/.relsPK-!};7!drs/slideLayouts/slideLayout1.xmlPK; .PK![Content_Types].xmlj0Eжr(΢Iw},-j4 wP-t#bΙ{UTU^hd}㨫)*1P' ^W0)T9<l#$yi};~@(Hu* Dנz/0ǰ $ X3aZ,D0j~3߶b~i>3\`?/[G\!-Rk.sԻ..a濭?PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK!ŖL=7theme/theme/theme1.xml[[6~L{c ÙdiL;9YcCﻺadlɡIڞIdyZIZq^|(iUї/ ]Kˤ~ZrL7zY%kj=kb$Ѝ1-]Up b[OP,LpRJ|QV&ߗ .`mHGRD}z7ڒj~Idzݠ/}qr@}q9.}oE;s Q$0Ae{B9m$~k`47 j /YO5|Q${wfdF/Siť;]UzQ | VQ:9wU@|(pZޚu bKqu%Y/;嬺O`TL$3E~):ɦ*-N;C1&In_cڿ6{arpF;V |Q7eȵlpڲnN 1ELZ?o%S[RӨHS {8tv aDTb$HdYBY6eC&/Ñ93G\VGIἯn.%v:9΢>mtZ|uޔ{]im?iŇ ͷ!Ӏ5ey8fC,"<n I?\4eGC6oڍ]c0%Y&[b=2d}Hkmn 1TCڢk`\ g rQ|_knLZ}:i:MetcZ[F cz7GkK}!pHhY6~LZ/[x"xܷdxܓܥ$)8t$4=B!qBF3&d4"lly ]`4"(rft'T/qtyxN=BMQ@qi`NSbzĸQ_4!Ɗcdel v`AhQft9L8jNքo}r}i?)=;~t3II5ȤXfYO'cKȬDJآRN^=ъH16F-΂C {` XacRdC|ƗF~ʊO(!yw(eo_$CQ"Yv};k݆U2gZ@%\>4XL4I bzC77K`2)"6K =D9@ <_ x=6[CqYw`dճaw d6 %l(t:a5lGR!&lrvO5W2|YsI.nQ~6lGlجXFZ };Gb<66ͤ6fDf* dC-K `o;66o|gywϟਐ)z6OW)6NP6p |졔tm|?p%lY+I\z6aC$@$@$'P4`kwWac*Z.M"H^/ E ^{oI~/MlT&L֯:-48l"7ʦ%i[ظWacUf ;Qڻ9bYҥd#l|#eTV!kӭ8lƒLjlg*lKܜ#?H8y93mb+z%[S ;'qU GOmל JXh#l g%{ |q\'#- 2=B7t^ۄ, N~ gE&t-"?4 ΠMfrAsѺo_p?yjŝ & Xg3PK!*8 _rels/.rels 0DnzЃXmlo0of5OIw AN{cݠv=m 838yG 6U} ShLq`L)d=Ҍ\@.;3, ;$e͂): vq}j:zɥ'k茜(f,ƁXA6\m>PK!`.Xޏ$!drs/slideMasters/slideMaster1.xmlMr0 cV1oz`iYq+9Qkl  %Tpo\H EhB7 !IH` ݋4=>Ox7BZ{IR+"˷J@kWX]Mi"I~뮞^wa/ sBug\djV{a7UZp>!_5|e~sM ҠSo}WՂCN| <p{/L]V`=n; ʝJҤj>Wn+ orAr]hM1ѝbg-_:G, ޲xHT1@el+b-R2td۩w 2YjŹ1l`MM; [#kQ\H %}񲵗U.dEG_h PK-!(b[Content_Types].xmlPK-!*8 *_rels/.relsPK-!`.Xޏ$!drs/slideMasters/slideMaster1.xmlPK Default Design/0 3"+"@(  @ @ P? Rectangle 82945z%   X C   x @ H}?Rectangle 2"pjPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!,S1 drs/shapexml.xmlVo0~M!*TЕu8ؑ0}wvR*I<$Nﻻ.\rL1omq&TLmirfVb̕7ϟ *cuMoE.B[MͦYarO.Vk6saj*V~iXy39|12H:YaB;[Q᝱`J M.GMI!#r[l;H(qN]8CjM!igwtv,1oYLw,F[oo# ,Y~Fs BuY1䡈a#!x\R1-2j™qV׌HV 1{r2lMD Ռ][)*j/@M}X̂/Щg*~˚6CO^!Q#Ҙ6P3#ET+7B4gVUfܲVY*>RBEnѯ[L5ـadʺ.oy:>Xx}x!A V(={Aӹ5:a7޴fy>8'\y)Q0X]g`\ u(4`k+l' h/pPU";Zq VȌ6VL:5)]gReKtSa.bߢDb -JxITk/b$%W g3Cl+!aZ߇) (~W~:Td h}ۅߙ/)PdqPK!drs/downrev.xmlD]K0Cx\b [W EЮ M1eݿ9ͨ$ngЕn(&ӜIm`XA/B&)І`S} X6N0E`0!sc:=]̊m+(| x\j/|qNKC{sYdSOO xPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!,S1 drs/shapexml.xmlPK-!Ndrs/downrev.xmlPK_ ?%  p* C    @ V1? Rectangle 82947"@XK   @ H,Ȓ?Rectangle 4"PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!E\ndrs/shapexml.xmlXMo0 tZۉ1NhwicˉY$9KGIN6 R+٤'>dÔ.HitRD&R,Szw{y4D9p)XJϟND )]S'A@˚ RU`V-Z1̈́q*p JA'뙲z3SS:D@1oXwD1ZP_ ~bzP!ñ$ [h! (E۔۹~.vA-Tu8 $(pTR0 ,H֐ a8 paz,ֵV\1]* 7 L|>qz6lϑJi)}u6b-#T(/$Oi,dzȢl!6:fnvX`wq@n_ &`7n7.#R_x9%9+na1qӐ`*7)0gn pTh8eZC}㎋yYLf!e~\#DK^v\yַ/ܧ^(P{Zhik2odK%i{ 20L2d-6rowmpo{V^qoliK:u*J{"wRy^;wx0λ1Q kK;t/C1zDxdN2d>do??pPד_PK!_jjdrs/downrev.xmlDKK0!\8΃N b:e$N7pn=9V nfTY|+{Ұ۞mx$<&ޡl4 lPr;*UH|45-{z+:_4|K2V1CꪗǮ[`bprcZ/·bDvWbx@/xg`   PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!E\ndrs/shapexml.xmlPK-!_jjydrs/downrev.xmlPK )  RClick to edit Master text styles Second level Third level Fourth level Fifth level!    S  @ Vr? Rectangle 82949z   X C    @ NL?Rectangle 6"PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!JGeJ drs/shapexml.xmlVMo0 tMtv~cˍY$9K;Iۡa@v\,R#H xvęP.*u/w׃9g֑*Hj%24yچᬲisM:|'jou#d659|acʑZFpf]w:lci^S˒x1ǨCtPP*^a4OrhL( #o1}bT JRJuY$7fIq:`3y8yeAkR92S*۸pdA&/#y62!B$IwХvRF]e<j:! dV!~,nNûR:2,{ hE2x`PRK J܇)Ns&֪͊[*$$CM{L׹cd}.~Xu6j8,P?um{)1T}n-8FR+رJKYc9_ftp5 &d9Uru$Q!ބAUm]k |e\M).XlUbg=Fқl/܁a9auMN*?e(>-Y!+?Q(Fү=0SJtܱZV02q`B(KL>JuynnXTR@oj5.vAQvAZ=>߅99kX!? 6 d=⟄m.~PK!1drs/downrev.xmlDQK0Co.ˆL2|Ve-6IMpzRкh3uedk>I8/AX./"f;_.RW5u*C5V:161UAш7 V q[?|(DQ'ί; '?@0l62>Q$;%a[Yr`@W?PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!JGeJ drs/shapexml.xmlPK-!1gdrs/downrev.xmlPKx ?  p* C   < @ 0.k ?"PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!7drs/shapexml.xmlAn1 EHC=$S$Fa #'J7Ă;_zϿމ+<Ь1r "d.0icvlSNV=PK!Bdrs/downrev.xmlLAK@B2ovb4R<(m{fM4;viwK|0Ǜh;1hZng͵S- #uv,'WxM4"epIBc#іNoPy:l]-^4F׿<h +{3R^ODcLmvn*NBZgNIJ?PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!7drs/shapexml.xmlPK-!Bdrs/downrev.xmlPK I}OPM80___PPT10.q;  PK![Content_Types].xmlj0Eжr(΢Iw},-j4 wP-t#bΙ{UTU^hd}㨫)*1P' ^W0)T9<l#$yi};~@(Hu* Dנz/0ǰ $ X3aZ,D0j~3߶b~i>3\`?/[G\!-Rk.sԻ..a濭?PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK!,߼etheme/theme/theme1.xmlYKo7 Hȁ%Kq81,%E.˘\ߊX@Ѵ@o=m$@/qM]ֵ!~fr~4.DG4I3nֻ\*!)A0=$J囵 aK<'|rb"Emjkz֬fp S4֤VI?`)B&Fx3 6:lh<}&f$ExLu7 S@ X=:\3")90 Acg8 +l e~]oxFkoXR%z^d%|w<Y|g ?ixJu 9dn%|@籣ELy΋b dX Lq1njN&;ʥ!- P\ur {컗Ϟ>xzӇO`8݉/>B?ţϫ?Y5P_<_~۷*O\Dl3 kN&'3X k)x' \+xG@}^%b {]OR9qQ ׵,YW 3wQ><f9FZEO>Ù1ɈB?$bR |]zV.ɘNhZLڥ)JA6{wP*wȑB1a2^3*1N7J ODŽq4Usn qunc'Vq~OpWaG4K\B}{~ٹCm{*-D K^Ni"\L3u<"⻃g>x_ށ޷7xkyj]Yϱ is)elN!M,aÈ0癓 b$dFIbYP\vxhؕ=pSg9vbs,55š R0U5R+KkLM.ՄNA܁ Hn¥[^d#b2 iK+ v`\#Gz;iei8JVR /ij279YA:@!λ"xJspԽf1\Jب0M/ypcqNye R`0Hdd_kC̼&mZRL$Tr|%186\Z+8(KN[1l}\Vx 7uu.Ҽ9ڀ)[VѼ%J])B#L2eem/\ poFz}Cz\C=rDž@p_1Y.,hF%} 3Q&h.$+)L8 ˼u01u\/+{cw}Ɣ46¯9%#cdhn PK! ѐ'theme/theme/_rels/themeManager.xml.relsM 0wooӺ&݈Э5 6?$Q ,.aic21h:qm@RN;d`o7gK(M&$R(.1r'JЊT8V"AȻHu}|$b{P8g/]QAsم(#L[PK-![Content_Types].xmlPK-!֧6 +_rels/.relsPK-!TGtheme/theme/themeManager.xmlPK-!,߼etheme/theme/theme1.xmlPK-! ѐ'j theme/theme/_rels/themeManager.xml.relsPK]e h   D (  D D P)? Rectangle 83969z%   T B     D PD9? Rectangle 83970 ?%  V B     D V@? Rectangle 83971z   T B    c  D V=? Rectangle 71684"QKPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!9{:c  drs/shapexml.xmlVn6?e`'t70PeH'E璲' b]M%^9X)v֕F'ÙԙKIׇք3΅2Z&\>3W3nV'|}=k]pL-5 c+h7J'q*u:v]R+8Ӈu+;ܖJ]ކPҗ;b {$Jx,uzÙP)6T l*H*+LC5W7` ؕ9S1h<{Q. 41҃H\BPG'dk3ʷrGB3 RNˇpÃ}:jz]g  BsquP]bvt0>Rd,U#:0W]!I~ZQ寕K'$/myl EUoE|=#9M>y JZ *6PxĜ™%q49' %A镰K*as\Cay r{ @"h-R/.oB6Md*yKw@DAwPF>(b'EHbV<M&ݛho 7֠?&y5-:^5X׸ɅTvep[_PM>7HfVϕ!g[x$>_SКjx>BsDd7},Df<--^J7kS$B?hR jJXAhozv &WPK!8g drs/downrev.xmlDN@E&3qc`F(H&[ PƄ;[tJ#Z`4 .ht {@Zpi42ˋ9_ޡ]޷Qq74-+UVTX~J ;xX7 \?t"Y1v}=>!$;EkIW\3 &qx\lm#R  PK![Content_Types].xmlj0Eжr(΢Iw},-j4 wP-t#bΙ{UTU^hd}㨫)*1P' ^W0)T9<l#$yi};~@(Hu* Dנz/0ǰ $ X3aZ,D0j~3߶b~i>3\`?/[G\!-Rk.sԻ..a濭?PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK!aYKtheme/theme/theme1.xmlYMo5#d4uS%ڴQv[ԣw;3ޤ( 7J\ʯ AxmYlKPթۏ_{/_3tHDK"EZpI3^NTƻ\*#9A0eJ덆5xI 6" EH>9k,7V#ǴPs{s<1AC-4ڨ<J1-T# *9XߤHG]&!fiq+SmsU ,'ǭ5<q 7 \wl|B ^{1s@ve۞=dsromPhq0n6pU)dNnw:3dZ3ZŘʫ [s\l@?0hqI8bFGj{:*s.$cAKՉ>(1Lދ߽xx? 7!͉D79f[NFF 3LE*qQD DcH VALm|"H0pcVflUO-ܔTyrW_6ԕP +Ui$TKYr}Uoze+U`^'Beh-И+.0|qT{9OS$(0*0e\aS1l%] e [Nʞ!aCA)RW" q -1Ju$K-qͣfkvpuk@!ߖ,.Ԥ4[,_sKs w/c$U=]Ehh,MNV~*bf$|S2 oc¬707`~Fr᣻g܃c7d`\Yk5PK! ѐ'theme/theme/_rels/themeManager.xml.relsM 0wooӺ&݈Э5 6?$Q ,.aic21h:qm@RN;d`o7gK(M&$R(.1r'JЊT8V"AȻHu}|$b{P8g/]QAsم(#L[PK-![Content_Types].xmlPK-!֧6 +_rels/.relsPK-!TGtheme/theme/themeManager.xmlPK-!aYKtheme/theme/theme1.xmlPK-! ѐ'P theme/theme/_rels/themeManager.xml.relsPK]K m 0aN0   0 (  0^ 0 # L0e0e ?Shape 121859"b\PK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK! $..drs/shapexml.xmlT]O0}u6"E6Bgt84Ա3-~N M$^!^~s?N϶6Z ,V::R%IDƔfgϟNԶ|Mی-k8|) J!nB9rxq2GqCb3S]/Du 0pr<x_ԨGF9J wcM tOp̯K-3#RQC-nZrs Һ=K$Gd0`!39@ tIժuL+:Enw=[! \i΃SAAT.1 x`E0/ؖ/6Á BTmf՞WvX_Js |"^!5R0qṰ "ظY~00Z7uTd1r,8NEPv&kȲԫ h% =M[•[O;-=߲3F*ȶqRP!JJ_Rv t7V˺7aIvIPX<&*ݞ\S$82<H竏B:"xO7#" B 2cMKmg?PK!/ drs/downrev.xmlD[K@C8/b7i5mb[Q om4{EO{FNhE!qUi&TM᭜_f9a4L''c̙>wk_G\MN. *x[m% mMC`˖ 8%#"Q0Ѡ voIl/c.Ն=Sz~ a }9JD'V7f\>//$K򸱂<b PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-! $..drs/shapexml.xmlPK-!/ 8drs/downrev.xmlPKQ`   @ 0 # ,Օ0e0e ?Shape 78849D `   @H 0 0޽h ? 33___PPT10i.Ck+D=' f = @B +" PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK 0aN0 $(  r  S ߒ  `}   r  S ߒ  `  H  0޽h ? 33___PPT10i. '5 +D=' f = @B +! 0aN0   <U (  <S < # D0e0e ?Shape 50177"WQPK!'[Content_Types].xmltMn@ zU2 LXs851I3 w{m J , a_""; ϏpO$&YZ=(eLY9iDلZZY4Nx jv~6(8`Ja𨹩rReN><Ir f=7_PK!1_a _rels/.relsj0 ѽqCNo^K [ILcX&m߾0XFo;>0xM e`|X}đ I`߽N4aG2$RKIZ)4(M9`ctB{m:f@`3n|O,ܗr޾jxR0T ,0@}WBLǬ5vPK!3drs/shapexml.xmlTN1}ZA.BVl VPD๚xdN-Jy\]|}u:N,dM4RCW[>t+Ԟ<ԪvO:G*xLgIܬUEΏ!kwFp5.2tm:7q'W 8=D5W ZTpȝKɆl W#M`t2쏎[dMi(3eB!H94@x&>G'A/` 8x)3d~si=?8:8w?WdA7 9 gfAՕQ9iWs.6S7'zֈz)gYAD>_`2VD n T N§0]!;϶-[o}4їv4_D9/FPj& LWZ @aAp քg{hyoq)]ۗNkՕwH|5۾׀z*&6n":)L&e.WuU* 9~i bdYj,J-i[^aߩj+c[UaiFSFJI_m+t㌪py UTZj U#!^e)m5-cĕV/ nG!\RPُ IBcM.d Ǫ4HPK!pV drs/downrev.xmlDK0 KLm]69TNķڲKH5qEPCr F[۪y%԰x.+B#style.visibility<*<!%(Dc ' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*<%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<6%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<6L%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<Lb%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<bv%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<vx%(+8+0+<0 +"  PK!/7[Content_Types].xml=k0BZlJ)34֏!|E퓐.!=;J@!yiS/+\h=V_'20BϘY6elLvN i1&CU=CoQ}Bw$ǰ$T X ab H"tww$\+nb$^S$r֊l..y1_I^d53˝PK!֧6 _rels/.relsj0 }Q%v/C/}(h"O = C?hv=Ʌ%[xp{۵_Pѣ<1H0ORBdJE4b$q_6LR7`0̞O,En7Lib/SeеPK!TGtheme/theme/themeManager.xml A 0@ѽDд;wC3dRP=Y~qv.5dp4(% 8AF(fa aL[9</R YX[ b]RKֳxt"^PK-!/7[Content_Types].xmlPK-!֧6 "_rels/.relsPK-!TG theme/theme/themeManager.xmlPK 0aN0 @$(  @r @ S Ȝ  `}   r @ S | 0@   H @ 0޽h ? 33___PPT10i.s`+D=' f = @B + 0aN0  t(  ~  s *,=  `}  =    S = p <$0 = B  s * C"?P `,$D0 class Meeting { int day; int time; invariant 0 d" day<7 '" day==6 1200<= time; void Reschedule(int d ) requires 0 d" d < 7; { day = d; X.P(this); if ( day==6 ) time = 1200; } } <Z  3f    !t    ?  4  * =>  BG]H!f ?S"? _ /y  H 0     BGHf ?S"?  F0   H  0޽h ?/  ̙33___PPT10.*?`+W[%D' f = @B DF' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* U%(+8+0+ 0 +  0aN0 f^  (   x   c $+ P      s *, <$@0     0 P` ,$@0H   0޽h ? ̙33___PPT10.*?`+vDZ' f = @B D' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* <%(+~ 0aN0 xp 4(  4x 4 c $A      4  < ?A S"  `<$D0  X 4 0@@P H 4 0޽h ? ̙33___PPT10n.*?`+YDB' f = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4Am%(+  0aN0 d(  ~  s *c  `}       Ht[A  "T  ?P   `   0xq? ,$D0 DTr[[unpack o]] = assert o.inv = valid; o.inv := mutable ^D (N          0t? 0 ,$D0 PLTr[[pack o]] = assert o.inv = mutable; assert Inv(o); o.inv := valid xM3fh         H  0޽h ? ̙33___PPT10.*?`+wQD~' f = @B D9' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* C%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*M%(+1 0aN0  0 (  0r 0 S   `}   F 0 s D0e0e  "B0e ?2``   *=>0 0 <l?C"?-[Z ,$D0 p,void Reschedule( int d ) requires inv==valid 0d<7; { expose(this){ day = d; if ( day==6 ) time = 1200; } }  3f%%@  0   H => 0 00 ,$ 0 ESpec# uses expose, defined by expose(o) s; = unpack o; s; pack o;zF     &"   "  0 <Hf8.d,$@0 U :Meeting        0 0~e,$D0  0 0d3 ,$D0  0 01 \| ,$D 0  0 0j9 ,$D 0 0 <Tq[ N ,$ 0 b x.P(this);     0 0Xŝf H ,$@0 KValid    0 <ȝ3 P ,$@0 MMutable   B 0 s *D9U?,$@0H 0 0޽h ? 33-#%#___PPT10#.*6+-YD!' f = @B D|!' = @BA?%,( < +O%,( < +D ' =%(DW ' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* 0%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*0%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*0%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*0%(D' =4@BBBB%(E' =1B B`BPB1:Bhidden*3>+B#style.visibility= `B<* 0D' =1:Bvisible*o3>+B#style.visibility<* 0%(D' =%(D)' =%(D!' =4@BBBB%(D' =,543*3>Bfillcolor=@BPB<* 0D' =1:B solid*a3>Bfill.type<* 0D' =1:B true*]3>Bfill.on<* 0D' =4@BBBB%(E' =1B B`BPB1:Bhidden*3>+B#style.visibility= `B<* 0D' =1:Bvisible*o3>+B#style.visibility<* 0%(D' =%(D' =%(D' =A@BBBB0B%(E' =1B B`BPB1:Bhidden*3>+B#style.visibility= `B<*0D' =1:Bvisible*o3>+B#style.visibility<*0%(D' =4@BBBB%(E' =1B B`BPB1:Bhidden*3>+B#style.visibility= `B<* 0D' =1:Bvisible*o3>+B#style.visibility<* 0%(D' =%(D)' =%(D!' =4@BBBB%(D' =,54f*3>Bfillcolor=@BPB<* 0D' =1:B solid*a3>Bfill.type<* 0D' =1:B true*]3>Bfill.on<* 0D' =4@BBBB%(E' =1B B`BPB1:Bhidden*3>+B#style.visibility= `B<* 0D' =1:Bvisible*o3>+B#style.visibility<* 0%(D' =%(Du' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*0%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*0%(++0+00 ++0+ 00 ++0+00 ++0+00 ++0+00 +< 0aN0 @8 <(  <x < c $      < s * % `9<$0  X < 0 >H < 0޽h ? ̙33___PPT10d.*?`+XFD' f = @B D' = @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<*<%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<!%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<!+%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*<+:%(+8+0+<0 + 0aN0 D0(  Dx D c $  `}   x D c $ 0@   H D 0޽h ? 33___PPT10i.s`+D=' f = @B + 0aN0  D(  ~  s *&  `}     s *'  <$0    0+ M S ,$D0 <class Person { int freeDay; Meeting next; invariant this.next != null this.next.day != freeDay; }kZ 3f               =>  0 M^ , 0class Meeting { int day; invariant 0 d" day<7; void Reschedule(int d ) requires inv==valid; { expose(this){ day = d; } } }Z 3fZ  %  '    =>H  0޽h ? ̙33 | ___PPT10\ .*?`+D ' f = @B D ' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*.i%(D' =%(D)' =%(D' =A@BBBB0B%())))?D' =1:Bvisible*o3>+B#style.visibility<*.%(D%' =%(D' =%(D' =4@BBBB%(D' =,54*3>!Bstyle.color='`B@BPB<*}D' =A@BBBB0B%())))?D' =1:Bvisible*o3>+B#style.visibility<*.r%(+8+0+0 +` 0aN0 {$.t@(  tr t S ^  `}   " t H`?#" `  X : Meeting 0    rB t <D?" " t Hd?#" `  W : Person 0    xB  t BD?" L  t c $   t BZk  Jnext    t <o}^ next.day != freeDay8   4    kl  9  t f ,$D0T 6 ,)   t#  "  t Blu?#" `6 ,)  n : Foo0 &   zB t <D?"F ,F ZB tB s *D 9  t Bn8{2   Ibar    t < d bar.day >= 5    B t 6D ,$D0 t B,$0 xcall reschedule(4)6   8l V  tV,$D0ZB tB s *D>w<ZB t s *D>V8l  [  t [ ,$D0ZB tB s *D> K ZB t s *D> [ l   -t  ,$D0fB t 6D  t B  xcall reschedule(4)6    t BZL ,$0 jcall re- schedule(4)$    !t c $  ,$@0 "t BZ  ,$0 Kowner    &t 0f)Pe),$@ 0 KValid    't 0Ȟ3) Qe),$@ 0 MMutable    (t 0-Pg-,$D 0 Q Committed     )t <C=,$0 Linv =    r *t 0 ,$@ 0B .t@ 0D  ,$D0H t 0޽h ?/@ t!t 33GG___PPT10G.n9+CDE' f = @B D>E' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* t%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*-t%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t%(D' =%(Dd' =%(D' =4@BBBB%(D' =1:Bhidden*o3>+B#style.visibility<*t%(D' =4@BBBB%(D' =1:Bhidden*o3>+B#style.visibility<*-t%(D' =%(D@' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*)t%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<**t%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*&t%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*'t%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*(t%(D ' =%(D ' =%(D!' =4@BBBB%(D' =,54f*3>Bfillcolor=@BPB<*tD' =1:B solid*a3>Bfill.type<*tD' =1:B true*]3>Bfill.on<*tD' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*!t%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*"t%(D!' =4@BBBB%(D' =,54*3>Bfillcolor=@BPB<*tD' =1:B solid*a3>Bfill.type<*tD' =1:B true*]3>Bfill.on<*tD' =%(Du' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*t%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t%(D' =%(D' =%(D!' =4@BBBB%(D' =,543*3>Bfillcolor=@BPB<*tD' =1:B solid*a3>Bfill.type<*tD' =1:B true*]3>Bfill.on<*tD!' =4@BBBB%(D' =,54f*3>Bfillcolor=@BPB<*tD' =1:B solid*a3>Bfill.type<*tD' =1:B true*]3>Bfill.on<*tD' =%(Du' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*t%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*.t%(D' =%(Dy' =%(D!' =4@BBBB%(D' =,543*3>Bfillcolor=@BPB<*tD' =1:B solid*a3>Bfill.type<*tD' =1:B true*]3>Bfill.on<*tD' =%(Dy' =%(D!' =4@BBBB%(D' =,54f*3>Bfillcolor=@BPB<*tD' =1:B solid*a3>Bfill.type<*tD' =1:B true*]3>Bfill.on<*tD' =%(Dq' =%(D' =A@BBBB0B%(D' =1:Bhidden*o3>+B#style.visibility<*t%(D' =4@BBBB%(D' =1:Bhidden*o3>+B#style.visibility<*.t%(D' =%(D' =%(D!' =4@BBBB%(D' =,54*3>Bfillcolor=@BPB<*tD' =1:B solid*a3>Bfill.type<*tD' =1:B true*]3>Bfill.on<*tD!' =4@BBBB%(D' =,54f*3>Bfillcolor=@BPB<*tD' =1:B solid*a3>Bfill.type<*tD' =1:B true*]3>Bfill.on<*tD' =%(Dq' =%(D' =A@BBBB0B%(D' =1:Bhidden*o3>+B#style.visibility<*t%(D' =4@BBBB%(D' =1:Bhidden*o3>+B#style.visibility<*t%(++0+t0 ++0+t0 ++0+t0 ++0+t0 ++0+"t0 ++0+&t0 ++0+'t0 ++0+(t0 ++0+)t0 +  0aN0   H(  H~ H s *  `}   L C6 t)  H#   " H BT?#" `C6 s)  X : Meeting 0    tB H 6D?"CF tF L 6 ,)  H# J="  H Bt?#" `6 ,)  W : Person 0    zB  H <D?"F ,F   H TZ ?"opj  Sowner0     H 0P 0 Y,$0 <Z  r H S l     X H 0=NO H H 0޽h ? H HH ̙33___PPT10.D+Dy' f = @B D4' = @BA?%,( < +O%,( < +Dk' =%(D' =%(D' =K@BBBBPB0B%(/%(D' =1:Bvisible*o3>+B#style.visibility<* H%(+8+0+ H0 + 0aN0 kc (  ~  s *  `}     s *   P<$@0    s *h  4 ,$D0 class Person { int freeDay; Meeting next; /*implicit*/ invariant next null next.owner = this; & }~xZ "33333Z    C    =>  < ~+x,$0 Mrep 3  H  0޽h ? ̙33#  ___PPT10 .*?`+KD ' f = @B DR ' = @BA?%,( < +O%,( < +D ' =%(D1 ' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*O%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4r%(+8+0+0 +)  0aN0 P w(  ~  s *V  `}      0xZ  S"   <$D0    s *  S"  <$D0     s *ܒ? ` ?unpack(o) and pack(o) and change inv for o and o's rep objects N      H  0޽h ? ̙33___PPT10.*?`+F9D~' f = @B D9' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*:o%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(%(+  0aN0 0 %P(  P~ P s *  `}   r $P S   0  X %P 0@H P 0޽h ? ̙33___PPT10i.*?`+D=' f = @B +  0aN0 [S x(  xx x c $  `}    x s *xA   <$D0  X x 0Mw ! x <L8,$0 ;This addresses the transitivity problem of modifies clauses< < < H x 0޽h ? 33___PPT10. +1W`D' f = @B DF' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*x%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*x%(+8+0+x0 +& 0aN0  @(  @r @ S   `}    @ S   <$D0  X @ 0G H @ 0޽h ? 33___PPT10n.S\+YDB' f = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*@%(+? 0aN0 ` C (  ~  s *  `}     s *8 0  >0class Person { int freeDay; rep Meeting next; invariant next null next.day freeDay; int doTravel(int td) requires inv==valid; modifies this.*; { expose(this) { freeDay = td; if (next!=null) { next.reschedule((td+1)%7); }; } Z  )  O     4         4      O =>  0'?S ` yuclass Meeting { int day; void reschedule( int d ) requires inv==valid; { expose(this) day = d; } }vZZ    #    "  HG?#" `F X : Meeting 0    rB  <D?"G"  N$LfG?#"  `PGC W : Person 0    B   fDvd @?#"  `G`  H$P ?" o Vowned by 0    L  c $C 3 0  ,$D0G PA +# PA,$@0T 6 ,)  # PAC"   HTd?G?#"  `6 ,)  W : Person 0    B ! ND3vv/?#"  F ,F T C6 t)  "# A" # BYf?#" `C6 s)  X : Meeting 0    tB $ 6D?"CF tF  8 6 P ,$@0 9 0 p ,$D0 C6 t)  %# @,$@0" & B^d??#" `C6 s)  X : Meeting 0    tB ' 6D?"CF tF  : 6 p ,$@0" . N`cfG?#"  `PAC,$@ 0 W : Person 0    " 1 H h?#" `@,$@0 X : Meeting 0    B 2 <D?"A,$@ 0 ; 6p ,$@ 0 ? 0 O ,$D0 A 0 [ { m,$@ 0" B Blf?#" ` 9,$D 0 X : Meeting 0    " C Bq?#" `@,$D0 X : Meeting 0    H  0޽h ?  ̙33##___PPT10z#.*?`+Dn"' f = @B D)"' = @BA?%,( < +O%,( < +Dx' =%(%(D' =%(D' =4@BBBB%(E' =1B BPB`B1:Bhidden*3>+B#style.visibility= `B<*3D' =1:Bvisible*o3>+B#style.visibility<*3%(D' =%(D<' =%(D' =4@BBBB%(E' =1B BPB`B1:Bhidden*3>+B#style.visibility= `B<*8D' =1:Bvisible*o3>+B#style.visibility<*8%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*+%(D' =4@BBBB%(E' =1B BPB`B1:Bhidden*3>+B#style.visibility= `B<*9D' =1:Bvisible*o3>+B#style.visibility<*9%(D' =%(D<' =%(D' =4@BBBB%(E' =1B BPB`B1:Bhidden*3>+B#style.visibility= `B<*:D' =1:Bvisible*o3>+B#style.visibility<*:%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%%(D' =4@BBBB%(E' =1B BPB`B1:Bhidden*3>+B#style.visibility= `B<*?D' =1:Bvisible*o3>+B#style.visibility<*?%(D' =%(D' =%(D' =4@BBBB%(E' =1B B`BPB1:Bhidden*3>+B#style.visibility= `B<*AD' =1:Bvisible*o3>+B#style.visibility<*A%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*B%(D ' =%(DW ' =%(D' =4@BBBB%(E' =1B BPB`B1:Bhidden*3>+B#style.visibility= `B<*;D' =1:Bvisible*o3>+B#style.visibility<*;%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*.%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*2%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*1%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*C%(++0+.0 ++0+10 ++0+B0 ++0+C0 + 0aN0 H0(  Hx H c $T  `}   x H c $ 0@   H H 0޽h ? 33___PPT10i.s`+D=' f = @B + 0aN0 }u ( (  (r ( S   `}   r ( S   `   - ( s *䵮?   ,$@0 u Example class Cell { int x; invariant x>=0;...} class BackupCell: Cell { rep History h; invariant h.last>=x;  i      Z     $   i ( s *®? p ` ,$@0 gObjects of type Cell have 2 frames: [Cell, object] type B have 3 frames: [BackupCell, Cell, object] * [h&M    8    ( ` ( 0 TB  ( c $D  .  ( B|ɮ   ,$0 0 Subtypes are allowed to strengthen invariants(1 .3 1   ( <xϮ  ,$0 Yinvariant x>10;   H ( 0޽h ? 33  ___PPT10 . hˬ+a D< ' f = @B D ' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(6u%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(5g%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(6u%(D' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* (%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* (%(+p+0+ (0 ++0+ (0 +0 0aN0  |(  |r | S   `}    | s \0e0e  #" 0e `   | s *?`P,$@0 hIdea: Reduce inheritance to ownership of frames. If B is a direct subtype of A, then B has a rep field A. But we only have one inv field, so: o.inv now represents the most derived frame for o which is valid, i.e. o.inv <: T means Inv(o) holds for the frame T and all its super frames o.inv == typeof(o) means Inv(o) holds for all of o s frames o.owner is now a pair (p,T); p is the owner, T the frame that contains the rep field that points to o.  GM/33aB     M    B    1             Q H | 0޽h ? 33___PPT10.pP~d+M{DZ' f = @B D' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*|^|%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*||%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*|%(+0 0aN0   "h  (  hr h S `v  `}     h HLu ?"x2 owned by the BackupCell frame0 &    " h H4VfG?#"  `  j : Cell (frame) *0     h <؃  Kinv   "  h Hf?#" `  : BackupCell (frame) *0 &     "  h H]?#" `  l: History (frame) *0    h <((  "  xpacked as BackupCell 3&     . h 0,+ {| Commiting c to p means then c.commited let (p,T) = c.owner in p.inv <: T  4                h <,( g " ,$D0 Xpacked as Cell 3  L h@ c $  h c $ ,$@0L h c $  h 0fr r  KValid    h 03r r  MMutable     h 0ܿv v  Q Committed    H h 0޽h ??` h hh hhh h hh 33___PPT10.. Qy+{DA' = @B D ' = @BA?%,( < +O%,( < +D3 ' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*h%(D' =4@BBBB%(D' =1:Bhidden*o3>+B#style.visibility<*h%(D!' =4@BBBB%(D' =,54 3*3>Bfillcolor=@BPB<* hD' =1:B solid*a3>Bfill.type<* hD' =1:B true*]3>Bfill.on<* hD!' =4@BBBB%(D' =,54 f*3>Bfillcolor=@BPB<* hD' =1:B solid*a3>Bfill.type<* hD' =1:B true*]3>Bfill.on<* hD' =A@BBBB0B%(D' =1:Bhidden*o3>+B#style.visibility<*h%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*h%(+8+0+h0 + 0aN0 0P(  Pr P S    `}   r P S   `  X P 0@H P 0޽h ? 33___PPT10i.~PP`Q+D='  = @B + 0aN0  l"(  lr l S >  `}    l  0d.  S" p p    l s *\'  S" pp     l s * ͪ? m%Given class T:S and o of type T. Then& & & C l <O ~ ]pack(o as T) claims every object that has o as its owner and its rep field declared in T <^ U X H l 0޽h ? 33___PPT10i.5 +D='  = @B +4 0aN0   0 P (  Pr P S M  `}    P 0O?   ^virtual void Cell.Set(int x) requires & modifies this.*; { unpack(this from Cell); this.x = x; pack(this to Cell); } P3f3ft    +          V P 0_?   Boverride void BackupCell .Set(int x) //requires & { unpack(this from BackupCell); this.b = this.x; base.Set(x); pack(this to BackupCell); } P (3f                             P 0q?   $void M(Cell c) { c.Set(23); } &%P!&   G P 6s$ ,$0 ?How can we verify the dynamically dispatched c.Set call? $@ >&3   H P 0޽h ? 33/'___PPT10.@>+gD'  = @B D^' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =,54*3>!Bstyle.color='`B@BPB<*P DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*P%(+8+0+P0 + 0aN0   H](  Hr H S T?  `}   r H S  l   X H 0; ] X  H 0  X  H 0   H B;04 %Only m.C contains the translated code0& 3&   H H 0޽h ? 33___PPT10i.^+D='  = @B +j 0aN0 ia`\(  \r \ S T  `}   G \ 0خ?`@ virtual void Cell.Set(int x) requires this.inv == 1; modifies this.*; { unpack(this from Cell); this.x = x; pack(this to Cell); } void M(Cell c) requires c.inv == typeof(Cell); { c.Set(23); } P 333  3      !                 H \ 0޽h ? 33___PPT10i.p@I+D='  = @B + 0aN0  L0(  Lx L c $ö  `}   x L c $ö 0@   H L 0޽h ? 33___PPT10i.s`+D='  = @B +A 0aN0 @00h(  x  c $ɶ  `}     c $pʶ  `<$@0  X2  0r eQ= X2  0 XD[ X2  0 ZF X2  0zX2  0f~j X2   0 < ( X2   0~ I L  @ c $=  L   c $= Z~ L   c $ Q L @ c $0 .~ R  s *>  L  c $  2  0fnm Y 9,$@02  0 p ,$@02  0 ,$@02  0   ,$@02  0j .5 ,$@0X2  0n  9  s *3>  ,$@0  s *3> p  ,$@ 0  s *3>& & ,$@ 0 @ c $ 3j ,$@ 0X2  0/ R @ s *>+ (  /R  s *>+ nX2  0 kX2  0q<L  @ c $]L !@ c $ ( ( " B CDEF||L,/#g&,YDg`8GYp$AZyWFp0MV9Y89}3,,.(39MZ o}-4`%ntv*rmk[<  i5hQCo;Z)I .$yH:Xd,2QJ*) y[rlLkD_8W1K&AE*9"p  XAz3[CUX@                                          B #@ 0D3>  ,$@ 0B $@ 0D3>} \} ,$@ 0B %@ 0D3>  ,$@02 & 0 ,$@0B '@ 0D>8s ,$@0 ( *BSCDELF~SSX5,-OAlBbb>{7+$ ,,pEf5DYcw vaUO` -A SQQ|LZKPCI?@)  ^tT"ONpV5 yxoWe,= KX<@@                           `" uj ,$@0RB ) s *D -X2 * 0 yX2 + 0 jV~2 , 0,$@02 - 0^J,$@0 . s *3>ICI,$@0B /@ 0D3>O,$@0n 0 BvC]DE<FvOO~:2#i9  CUyrJb>$5o 9nLrQ"+ZF3?BRR(P]]E1 "z(m/[B9B9HK\bmvutEtpk]N@* w] ] '3D)~:8<@                          `z ,$D0H  0޽h ?           !. 33"~"___PPT10^".4\+lD2"'  = @B D!' = @BA?%,( < +O%,( < +D$!' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*9h%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*#%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*&%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*'%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*,%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*-%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*.%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*/%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*0%(+[ 0aN0 P @(   x   c $  `}       0  S"         0  "6 ?  <$@0     <l C,$D0 @LPeer fields give rise to additional invariants, for Nodes e.g. next!=null owner = next.owner prev!=null owner = prev.owner But how can we reason locally?v O ZY        " H   0޽h ? 33;3___PPT10.9pI>E+JQ (D'  = @B Dj' = @BA?%,( < +O%,( < +DT' =%(%(D' =%(D' =4@BBBB%(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<*  %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*  %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*  %(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*  ,%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* ,D%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* DQ%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* Qx%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<* xz%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(+8+0+ 0 +z 0aN0   ` $. (  $~ $ s *D'  `}    $ s *D( U -S<$0   $ s *? 0 6  class Person { Person spouse; invariant this.spouse null this.spouse.spouse = this; & }jlZ 3f3f3f3f$3f@/      ABF    $    " $ H`5f?#" ` O x: Person spouse: 20     tB $ 6D?"z $ <?"Nb  $ NG`HdI@Ԕ?"N "  $ HH0f?#" `  x: Person spouse: 20     tB  $ 6D?"z  $ <?"^ F b  $ NGIHIԔ?"F. H $ 0޽h ?/@$ $ $$ $ ̙33$___PPT10.*?`+[W_D'  = @B DS' = @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<*$=%(+8+0+$0 +8  #0aN0 p((  (~ ( s *] }    ( c $^   <$@0  @ ( s *v pp  class Person { Person spouse dependent Person; invariant this.spouse null this.spouse.spouse = this; & }rZ 33 !@=       ABH ( 0޽h ? ̙33___PPT10.ڍ+EDZ'  = @B D' = @BA?%,( < +O%,( < +DL' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(H%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(HW%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*(W%(+  0aN0 0j(  0~ 0 s *T  `}    0 s *T `<$0   0 s *? `  @Z  X 0 0} H 0 0޽h ? ̙33  ___PPT10 .ڍ+[W_D '  = @B D ' = @BA?%,( < +O%,( < +DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*0%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*0Z%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*0 %(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*0 %(+8+0+00 +#! 0aN0 < 4 4 (  4~ 4 s *D  `}   & 4 s *  Y class Person { Person spouse dependent Person; invariant this.spouse null this.spouse.spouse = this; void marry( Person p ) requires pnull pthis this.inv = valid p.inv = valid this.spouse = null p.spouse = null ; { expose(this) expose(p) { this.spouse := p; p.spouse := this; } } }XZ33f333333f3f =D<      /                            AB 4@ B?#" ` B ,$D 0 Pthis.inv = mutable this.spouse = null >)0 4        4@ B?#" ` B ,$@ 0 Dp.inv = mutable p.spouse = null 4#0 4       4@ B?#" `o l@,$@ 0 Vthis.spouse.spouse=this p.spouse.spouse=p >,0 4    H 4 0޽h ? ̙33wo___PPT10O.ڍ+)&D ' Ҿ= @B D' = @BA?%,( < +O%,( < +D{' =%(D#' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*4%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*4D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*4D' =%(Da' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*4%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*4D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*4D6' =A@BB BB0B%(D' =-g6B fade*<3<*4D' =1:Bhidden*o3>+B#style.visibility<*4%(D' =%(Da' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*4%(D' =+4 8?dCB1+#ppt_w/2BCB#ppt_xB*Y3>B ppt_x<*4D' =+4 8?\CB#ppt_yBCB#ppt_yB*Y3>B ppt_y<*4D6' =A@BB BB0B%(D' =-g6B fade*<3<*4D' =1:Bhidden*o3>+B#style.visibility<*4%(++0+40 ++0+40 ++0+40 ++0+40 ++0+40 + 0aN0 8<(  8~ 8 s *ܾ  `}   ~ 8 s *tݾ  `  H 8 0޽h ? ̙33___PPT10i.*?`+D='  = @B +(0 08(  d  c $@XL     s *@ L(   " H  0.k ? ̙3380___PPT10.Q(0  88(  8d 8 c $@XL    8 s *ª@ L(   " H 8 0.k ? ̙3380___PPT10.Q(0  @8(  @d @ c $@XL    @ s *ƪ@ L(   " H @ 0.k ? ̙3380___PPT10.Q(0 @ T8(  Td T c $@XL    T s *\@ L(   " H T 0.k ? ̙3380___PPT10.!Q@ k0 ",(  ,d , c $@XL    , s *@ L(   tExplain: every prefix of an access expression is again an access expression and has to satisfy the same requirements u H , 0.k ? ̙3380___PPT10.r0mK tP'S9`L^b |e>Microsoft Research.-"Arial Unicode MS-. $2 D=Formal Methods 2006.-"Arial Unicode MS-. 42 O6Program Invariants, Callbacks,.-"Arial Unicode MS-. :2 U3"Aggregates, Ownership, Visibility .-"Arial Unicode MS-. 2 a _____________t.-"Arial Unicode MS-. 2 fJoint work with .-"Arial Unicode MS-. .2 f%Rustan Leino, Mike Barnett.-"Arial Unicode MS-. 2 fK , Manuel k.-"Arial Unicode MS-.  2 fXF.-"Arial Unicode MS-.  2 fZa.-"Arial Unicode MS-. 2 f\hndrich.-"Arial Unicode MS-. '2 ff, Herman Venter, Rob .-"Arial Unicode MS-. 2 fDeLine.-"Arial Unicode MS-.  2 f, .-"Arial Unicode MS-. 62 jWolfram Schulte (all MSR), and .-"Arial Unicode MS-. 2 j=Peter M.-"Arial Unicode MS-.  2 jHu.-"Arial Unicode MS-.  2 jJller.-"Arial Unicode MS-. 2 jO(ETH), .-"Arial Unicode MS-. 2 jY Bart Jacobs.-"Arial Unicode MS-. 2 jj(KU Leuven) and .-"Arial Unicode MS-.  2 jBor.-"Arial Unicode MS-.  2 j-.-"Arial Unicode MS-.  2 jYuh.-"Arial Unicode MS-. 2 jEvan ,.-"Arial Unicode MS-. 2 mChung (Berkley.-"Arial Unicode MS-.  2 m&) .-PropertiesS2WFV5BUWHK32LA==2 ٢EY٢EYItem  !Properties%2UJVJ0E0DNI4IQ==2 ٢EY٢EYItem -Properties/ <_0schulteschulte  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~xsd:element ref="dcterms:created" minOccurs="0" maxOccurs="1"/> This value indicates the number of saves or revisions. The application is responsible for updatitomXml"/>mentSummaryInformationDocumentLibraryFormDocumentLibraryFormDocumentLibraryForm pirationDatePublishingStartDate 2018-12-08T06:59:54Z2000-01-01T00:00:00Z storeItem ds:itemID="{B1094871-6B52-4668-83F4-DC48788C288D}" xmlns:ds="http://schemas.openxmlformats.org/officeDocument/2006/customXml"/>