ࡱ> 68FG7:(@ / 0DArialNew Roman tT0t"DArial Unicode MS tT0t" DCalibriicode MS tT0t"0DSymbolicode MS tT0t@DScript MT BoldS tT0tBPDTimes New Roman tT0t B . @n?" dd@  @@`` h`;'  X       - D1H       &1H1 *"     3      )/ ;,,+        0 3f3@ʚ;ʚ;<4dddd#0g4\d\dF: T0ppp@  <42d2dO$0 )___PPT12 %0___PPT10 ``6___PPT9{?  O  !Pj;Lecture 4 Towards a Verifying Compiler: Data Abstraction< <$ < | Wolfram Schulte Microsoft Research Formal Methods 2006 Purity, Model fields, Inconsistency _____________ 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) . Slides based on a presentation of Peter Mller given at MSR 5/2006 ^ Z Z Z Z(&4"J " I)"$  k     '  $  B   f3Review: Verification of OO Programs with Invariants44$ 4 nWhat were the 2 major tricks to support invariants? Which programs can we verify? What are the limitations? >4 :3 : o jData Abstraction using Methods  (Needed for Subtyping Information hiding 4 Z$ZZ)X     kEncoding of Pure Methods  ZPure methods are encoded as functions Functions are axiomatized based on specifications&7    l'Problem 1: Inconsistent Specifications  ( mProblem 2: Weak Purity  eWeak purity can be observed through reference equality How to prevent tests for reference equality? 2e8-3 f nProblem 3: Frame Properties  gResult of pure methods depends on the heap How to relate invocations that refer to different heaps?,h.)33 h o#Data Abstraction using Model Fields $ tSpecification-only fields Value is determined by a mapping from concrete state Similar to parameterless pure methods>N      p&Variant of Problem 3: Frame Properties''$ '  Assignment might change model fields of client objects Analogous problem for subtypes How to synchronize values of model fields with concrete fields?f7`7 @8  I rValidity Principle4  tOnly model fields of valid objects have to satisfy their constraints Avoids inconsistencies due to invalid objectsZE. 3#3R   Decoupling Principle4   Decoupling: Model fields are not updated instantly when dependee fields are modified Values of model fields are stored in the heap Updated when object is being packed pUR3#33p  tMutable Dependent Principle@   mMutable Dependent: If a model field o.m depends on a field x.f, then o must be mutable whenever x is mutable Dn$)3f     0 vThe Methodology in Action@   w!Automatic Updates of Model Fields " x Soundness  Theorem: Proof sketch Object creation new: new object is initially mutable Field update X.f := E; Model fields of X: asserts X.inv = mutable Model fields of X s owners: mutable dependent principle unpack X: changes X.inv to mutable pack X: updates model fields of X    c      c Z[  #  V  / z2Problem 1 Revisited: Inconsistent Specifications  3 Witness requirement for non-recursive specifications Ownership for traversal of object structures Termination measures for recursive specs  ,    },Problem 2 Revisited: Restricted Weak Purity--$ - ~%Problem 3 Revisited: Frame Properties&&$ & Model field solution does not work for methods with parameters Caching of values not possible for runtime checking Mutable dependent principle too strict  Summary  Data abstraction is crucial to express functional correctness properties Verification methodology for model fields Supports subtyping Is modular and sound Key insight: model fields are reduced to ordinary fields with automatic updates Verification methodology for methods (not yet ready) Partial solution: encoding, weak purity, consistency Future work: frame properties based on effectsZsx5ds(P35d&|    /"#$%&'(*,./02568;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  (     Txs: ?Rectangle 3073" `} :  X Click to edit Master title style!! F  N`v: ?Rectangle 3074" ` :  RClick to edit Master text styles Second level Third level Fourth level Fifth level!    S   N: ?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..f#PK!(b[Content_Types].xmln0 EAkP }l} m $_tI$svs^챐KkH$Q -G$oo1# ɩ5 J# \Qg0?0omRo?Y8 Jm i|TX+N3tr@9>?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.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-" nPK!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.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.xmlPKvPK!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.xmlPKpzPK!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!"G~!drs/slideLayouts/slideLayout1.xmlRj0BFI ؁>/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.xmlPK`PK!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.xmlSN0}٥RUE u })L7C}Dyŗ3g|`4eيo/7I+\OۋEۂvVV:~]eQXB;D_E4/r' mùh%j{0,g餄ċ' 5 qaaAF'P˃#gz nyMF̂1XL eZw  L`.Ŝayk F]yar8S$7Pq1T)(^;|bi@'X&U\-rdU*s92Hg?B4'z߱7ϸ)XG ~ƽ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=#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.xmlPKZ0PK!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!;bE !drs/slideLayouts/slideLayout1.xmlVn0?'z![i$%:BQɸvd;i 89]{v$[ mZM4 Py]a]f,W@&32@(IKQqsZ7BamQ[|ꇰ7+&Q4 {aKz(sΟ*Br̲lLhav$e7 6"!x0gW)g`W32ڭN Avj]7VM׫[ʂ@A.fS g녮g<l= bڲO|ymu9SN҅3[Fx7zU珆qR>zՁ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<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  @ Vd? Rectangle 82949z   X C    @ N?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 PDm? Rectangle 83969z%   T B     D Pw? Rectangle 83970 ?%  V B     D Vl? 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#R3\`?/[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 ; y 0aN0   0 (  0^ 0 #  ; 0e0e ?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___PPT10u..Ck+D=' = @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___PPT10u.. '5 +D=' = @B +q "0aN0    (  6  s *1 j+,$D0  class Rectangle implements Shape { int x1; y1; x2; y2; void DoubleWidth( ) ensures x2  x1 == old( x2  x1 ) * 2; { & } }Z   3f3f    X$     -   =>  s *A c*,$D0 bxclass Rectangle: Shape { int x1; y1; x2; y2; pure int Width( ) private ensures result == x2  x1; { & } void DoubleWidth( ) ensures Width( ) == old( Width( ) ) * 2; { & } }Z3f        +    1   =>~  s *B  f    s *b Mj e;interface Shape { void DoubleWidth( ) ensures ??; }<Z  3f3f 3f>     =>~  s *D  `}   g  s *lz Lg ,$D0 ginterface Shape { pure int Width( ); void DoubleWidth( ) ensures Width( ) == old( Width( ) ) * 2; }hZ      X     /  =>H  0޽h ? ̙33___PPT10..3/L+r@,D' = @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<*%(++0+0 ++0+0 ++0+0 +O #0aN0 B:@(  ~  s *  `}   ~  s *ܓ  `    s *Ȕ Gdg @M: Value Value Heap Value2!  !   s *ę c dg  0"this,par,Heap: RequiresM( this,par,Heap ) EnsuresM(this,par,Heap) [ M(this,par,Heap ) / result ]n                H  0޽h ? ̙33___PPT10u..@w=+D=' = @B + $0aN0 f^`$(  $~ $ s *H v    $ 0 m ,$D0 \Flawed specifications potentially lead to inconsistent axioms How to guarantee consistency?L>*33f3  b $ s *h̖    class Inconsistent { pure int Wrong( ) ensures result == 1; ensures result == 0; { & } }jZ  >  I  => $ s * / ,$D0 "class List { List next; pure int Len( ) ensures result == Len( ) + 1; { & } & }mZ p    E  =>H $ 0޽h ? ̙33C;___PPT10.. py+/+B#style.visibility<*$%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*$?]%(+8+0+$0 +  %0aN0 d\,(  ,~ , s *   `}    , s *4   <$D0   , s * Q W  }class C { pure C Alloc( ) ensures fresh( result ); { return new C( ); } void Foo( ) ensures Alloc( )==Alloc( ); { ... } }<Z    t  A       => , s *t(  ,$D0 !Alloc( this,H ) = Alloc( this,H )V"h         @`H , 0޽h ? ̙33#___PPT10..@{+>tD' = @B DF' = @BA?%,( < +O%,( < +DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*,%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*,8e%(+8+0+,0 +M  &0aN0 ;34(  4~ 4 s *Q  `}    4 s *R  @ <$D0   4 s *^ &3  Has( list, o, H )2    @` 4 s *u m   Tclass List { pure bool Has( object o ) { & } void Remove( object o ) requires Has( o ); { & } & }lZ     3 |   1    AB 4 s *  m  bvoid Foo( List list, object o ) requires list.Has( o ); { log.Log(  Message ); list.Remove( o ); }hjZ30         ABH 4 0޽h ? ̙33___PPT10z..#p!+YDB' = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*4/h%(+h '0aN0   < (  < < s *ߚ % z  class Rectangle implements Shape { int x1; y1; x2; y2; void DoubleWidth( ) ensures x2  x1 == old( x2  x1 ) * 2; { & } }Z   3f3f    X$     -   => < s * % | ,$D0 4Bclass Rectangle implements Shape { int x1; y1; x2; y2; model int width | width == x2  x1; void DoubleWidth( ) ensures width == old( width ) * 2; { & } }&Z   3f    $         )   =>~ < s * }   ~ < s *P  =    < s *` z  W;interface Shape { void DoubleWidth( ) ensures ??; }<Z  3f3f 3f>     =>_ < s * z ,$D0 _interface Shape { model int width; void DoubleWidth( ) ensures width == old( width ) * 2; }`Z      X     )  =>H < 0޽h ? ̙33h`___PPT10@..3/L+ MD' = @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<*<%(+p+0+<0 ++0+<0 + (0aN0   D (  D~ D s *M }    D s *N  `<$0   D s * Gq  Dhclass Rectangle { model int width | width == x2  x1; void DoubleWidth( ) modifies x2, width; ensures width = old( width ) * 2; { x2 := (x2 - x1) * 2 + x1; } }Z    +        B   =>t D s *pz ~q ,$D0 class Legend { Rectangle box; int font; model int mc | mc==box.width / font; & }ZZ r"           => D  v0e0e    BCIDEF @  > 8c8c     ?A)BCD|E||I/@  "< |# ,$D0H D 0޽h ? ̙336 . ___PPT10 ..3/L+ ВDf ' = @B D! ' = @BA?%,( < +O%,( < +DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*D%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*D%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*D8%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*D9X%(DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*DY%(+p+0+D0 ++0+D0 +  *0aN0 rj T(  T T s *ۮ Mq class List { List next; invariant list is acyclic; model int len | len == (next == null) ? 1 : next.len + 1; & }yZ   &          =>~ T s *,Ȯ  `}    T s *,ɮ ; `<$D0   T s *ˮ  dg ,$D0 H"X, m: X.inv = valid Rm( X, X.m )D% Z        H T 0޽h ? ̙33#___PPT10..+B#style.visibility<*T%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*TGu%(+8+0+T0 +& ;0aN0 nf@!(  ~  s *  `}   ~  s *4  `    s *2 ] ,$@0 h~class Rectangle { model int width | width == x2  x1; void DoubleWidth( ) requires inv==valid; { unpack this; x2 := (x2  x1) * 2 + x1; pack this; }Z$           W AB7z \ w   G,,,$D01"  B%f?#" `\ n %: Rectangle x1: 0 x2: 10 width: 10&0 &>   tB  6D?"d w 7z \ w    G,,,$D01"  B4-PP?#" `\ n %: Rectangle x1: 0 x2: 10 width: 10&0 &>   tB  6D?"d w 7z \ w   G,,,$@01"  BCPP?#" `\ n %: Rectangle x1: 0 x2: 20 width: 10&0 &>   tB  6D?"d w =z \ w   G,,,$D 01"  BHf?#" `\ n %: Rectangle x1: 0 x2: 20 width: 20&0 &>   zB  <D?"d w   HGJH:?" & ,$@0H  0޽h ? ̙33___PPT10..=/[+tSDE' L= @B D' = @BA?%,( < +O%,( < +DY' =%(D' =%(D' =A@BBBB0B%(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<*%(DF' =%(D' =%(D3' =4@BB*BB%()?)?D' =.O7 BBBBBaM -5.55556E-7 6.11677E-7 L -5.55556E-7 0.05792 *3>*B ppt_xB ppt_y=@0BBAApBBBA<<*D[' =4@BB BB%()))D' =1:Bvisible*o3>+B#style.visibility<* %(D' =-g6B fade*<3<* D@' =%(D' =%(D[' =4@BB BB%()))D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*D-' =4@BB*BB%()?)?D' =.I7 BBBBB[M -5.55556E-7 0.05783 L -5.55556E-7 0.12098 *3>*B ppt_xB ppt_y=@0BBAApBBB=<*D@' =%(D' =%(D-' =4@BB*BB%()?)?D' =.I7 BBBBB[M -5.55556E-7 0.12098 L -5.55556E-7 0.17349 *3>*B ppt_xB ppt_y=@0BBAApBBB!<<*D[' =4@BB BB%()))D' =1:Bvisible*o3>+B#style.visibility<*%(D' =-g6B fade*<3<*+8+0+0 +  ,0aN0 qi` d(  d~ d s *ۯ  `}   ~ d s *ܯ  `  z !   d !  ,$D0^N ViX  d !  " d HHPP?#" `ViX  n": Legend box: font: 5 mc: 2 #0 # # tB d 6D?"Viz d <?" gBb  d NGmH:MIԔ?"   N \ w  d ! :  1"  d BׯPP?#" `\ n %: Rectangle x1: 0 x2: 20 width: 20&0 &>   zB  d <D?"d w H d 0޽h ? d d d ̙33___PPT10z..=/[+ksDB' = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*d%(+5 .0aN0 t(  t~ t s *  `}    t s *  <+ class Legend { rep Rectangle box; model int mc | mc == box.width / font; & }rUZ 3f&@,       => t s *L Mq~ , class Rectangle { void DoubleWidth( ) requires inv == valid && owner.inv == mutable; modifies width, x2; { expose(this) { x2 := (x2  x1) * 2 + x1; } } Z  &                4 AB t HGJH:?",$@0" t TZH8I0>?"BF,$@07z \ w t T9 ,$@01" t BHf?#" `\ n %: Rectangle x1: 0 x2: 10 width: 10&0 &>   tB  t 6D?"d w z F,  t MS9,$D0"  t HPP?#" `F+ `: Legend mc: 2 0   tB  t 6D?"G , b  t@ NGHIԔ?"008,$@07z \ w t T9 ,$@01" t B81PP?#" `\ n %: Rectangle x1: 0 x2: 10 width: 10&0 &>   tB t 6D?"d w 7z \ w t T9 ,$@ 01" t B4PP?#" `\ n %: Rectangle x1: 0 x2: 20 width: 10&0 &>   tB t 6D?"d w =z \ w t T9 ,$@ 01" t B>f?#" `\ n %: Rectangle x1: 0 x2: 20 width: 20&0 &>   zB t <D?"d w z F, t MS9,$@ 0" t H8Bf?#" `F+ `: Legend mc: 4 0   tB t 6D?"G , H t 0޽h ?/@ ttt tt t ̙33___PPT10..*?`+溡D' = @B DI' = @BA?%,( < +O%,( < +Dd' =%(D ' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* t%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*t%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* t%(DF' =%(D' =%(D[' =4@BB BB%()))D' =1:Bvisible*o3>+B#style.visibility<*t%(D' =-g6B fade*<3<*tD3' =4@BB*BB%()?)?D' =.O7 BBBBBaM -5.55556E-7 6.11677E-7 L -5.55556E-7 0.05792 *3>*B ppt_xB ppt_y=@0BBAApBBBA<<*tD@' =%(D' =%(D[' =4@BB BB%()))D' =1:Bvisible*o3>+B#style.visibility<*t%(D' =-g6B fade*<3<*tD-' =4@BB*BB%()?)?D' =.I7 BBBBB[M -5.55556E-7 0.05783 L -5.55556E-7 0.11034 *3>*B ppt_xB ppt_y=@0BBAApBBB!<<*tD@' =%(D' =%(D[' =4@BB BB%()))D' =1:Bvisible*o3>+B#style.visibility<*t%(D' =-g6B fade*<3<*tD-' =4@BB*BB%()?)?D' =.I7 BBBBB[M -5.55556E-7 0.11034 L -5.55556E-7 0.16285 *3>*B ppt_xB ppt_y=@0BBAApBBB!<<*tD6' =%(D' =%(D[' =4@BB BB%()))D' =1:Bvisible*o3>+B#style.visibility<*t%(D' =-g6B fade*<3<*tD#' =4@BB?BB%()?)?Dw' =.?7 BBBBBQM -5.55556E-7 0.16285 L 0.5592 0.30974 *3>*B ppt_xB ppt_y=@0BBAApBBr>B\-=<*t+' /0aN0 |(  |~ | s *0t  `}    | 0ء zI pack X a" assert X null X.inv = mutable; assert Inv( X ); assert "p: p.owner = X p.inv = valid; & X.inv := valid; foreach m of X: assert $r: Rm( X, r ); X.m := choose r such that Rm( X, r ); end %3 33333 3333333333 33333  )                  `H | 0޽h ? ̙33___PPT10u..*?`+D=' = @B + 00aN0 |t (  ~  s *4Q  '}     s *   `<$D0    s * Nt  4F"X,m: X.inv = valid Rm( X, X.m )V$ t          H  0޽h ? ̙33___PPT10..*?`+YD^' = @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<* %(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*.%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*.N%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*Nf%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*f%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*%(+  20aN0 u m  (  ~  s *  `}   ~  s *       s * _6 "c iCpure int Wrong( ) ensures result == 1; ensures result == 0; DZ &  < =>t  s *\ #   2pure int Len( ) ensures result == Len( ) + 1; 3Z3f&  + =>&  s *  $ Y jpure static int Fac( int n ) requires n >= 0; ensures result == ( n==0 ) ? 1 : Fac( n-1 ) * n; kZ (3ft       @   =>  s * #   }Mpure int Len( ) ensures result == Len( ) + 1; measured_by height( this );NZ  @  *    =>m  s *$  # Z ypure static int Fac( int n ) requires n >= 0; ensures result == ( n==0 ) ? 1 : Fac( n-1 ) * n; measured_by n; zZ (3f        @      =>H  0޽h ? ̙33___PPT10u.. py+D=' = @B + 50aN0  '(  ~  s *X  `}   Q  s *M >P^ %pure C Alloc( ) { return new C( ); }j&Z&   =>  0\6  b  Pure methods must not return references to new objects (Compile time effect analysis) Provide value types for sets, sequences, etc.   H  0޽h ? ̙33___PPT10u..@{+D=' = @B +7 60aN0 *" (  ~  s *h  `}   ~  s *li       s *m    Xclass List { pure bool Has( object o ) { & } void Remove( object o ) requires Has( o ); { & } & }nZ   3f|   3    AB  s *x  Y bvoid Foo( List list, object o ) requires list.Has( o ); { log.Log(  Message ); list.Remove( o ); }hjZ 3f2         ABH  0޽h ? ̙33___PPT10u..@p_+D=' = @B + 80aN0  <(  ~  s *   `}   ~  s *  `  H  0޽h ? ̙33___PPT10u..=p+D=' = @B +j0 2*0(  d  c $@XL     s *@ L(   We want moduar verification*t  H  0.k ? ̙3380___PPT10.7/M(k0 P 8(   d   c $@XL      s *@ L(   " H   0.k ? ̙3380___PPT10.@(l0 p(8(  (d ( c $@XL    ( s *X@ L(   " H ( 0.k ? ̙3380___PPT10.(p_(m0 08(  0d 0 c $@XL    0 s * @ L(   " H 0 0.k ? ̙3380___PPT10.@G(n0 88(  8d 8 c $@XL    8 s *@ L(   " H 8 0.k ? ̙3380___PPT10.(p_o0 2*@(  @d @ c $@XL    @ s * @ L(   We want moduar verification*t  H @ 0.k ? ̙3380___PPT10.7/Mp0 *"H(  Hd H c $@XL    H s *@ L(    Analogous problem for subclassesh   H H 0.k ? ̙3380___PPT10.7/M(r0 0X8(  Xd X c $@XL    X s *@ L(   " H X 0.k ? ̙3380___PPT10.>/ At0 >6ph(  hd h c $@XL   * h s *8#@ L(   dExplain that decoupling violates program invariant if we dont have the mutable dependent principle8      H h 0.k ? ̙3380___PPT10.>/ A(v0 x8(  xd x c $@XL    x s *H/@ L(   " H x 0.k ? ̙3380___PPT10.lLw0 \(  d  c $@XL     s *4@ L(   FNot present in executable code  H  0.k ? ̙3380___PPT10.?,v (x0 8(  d  c $@XL     s *l:@ L(   " H  0.k ? ̙3380___PPT10.Q(z0 0 8(  d  c $@XL     s *@ L(   " H  0.k ? ̙3380___PPT10.(p_(}0  8(  d  c $@XL     s *D@ L(   " H  0.k ? ̙3380___PPT10.@G(~0  8(  d  c $@XL     s *J@ L(   " H  0.k ? ̙3380___PPT10.@ (0  8(  d  c $@XL     s * @ L(   " H  0.k ? ̙3380___PPT10.>p`B) 0 D<P!(  d  c $@XL   0  s *T@ L(   Explain that decoupling violates program invariant if we don t have the mutable dependent principle Addesses weak purity problem      H  0.k ? ̙3380___PPT10.>/ Ar0ã;PpC4,39EXq0N  6u#p6&( +P-/1j47L90=B?AC E&HVJ ~LfXRQ1:(@ / 0DArialNew Roman`` T0DArial Unicode MS` T0" DCalibriicode MS` T0"0DSymbolicode MS` T0@DSOh+'0, hp    (00Towards a Verifying Compiler The Spec# Approachschulteschulte204Microsoft Office PowerPoint@J@r2@EyGg  q T  y--$xx--'"Arial Unicode MS-.  2 q1."System-"Arial Unicode MS-. 3f2 ? Lecture 4.-"Arial Unicode MS-. 3f42 "Towards a Verifying Compiler: .-"Arial Unicode MS-. 3f2 ,5Data Abstraction.-"Arial Unicode MS-. 2 7@Wolfram Schulten.-"Arial Unicode MS-. "2 =>Microsoft Research.-"Arial Unicode MS-. $2 C;Formal Methods 2006).-"Arial Unicode MS-. =2 M3$Purity, Model fields, Inconsistency .-"Arial Unicode MS-. 2 X _____________t.-"Arial Unicode MS-. T2 ]3Joint work with Rustan Leino, Mike Barnett, Manuel .-"Arial Unicode MS-.  2 ]cF.-"Arial Unicode MS-.  2 ]ea.-"Arial Unicode MS-. 2 ]ghndrich.-"Arial Unicode MS-. '2 ]s, Herman Venter, Rob ..-"Arial Unicode MS-. 2 aDeLine.-"Arial Unicode MS-. B2 a', Wolfram Schulte (all MSR), and Peter .-"Arial Unicode MS-.  2 a[M.-"Arial Unicode MS-.  2 a^u.-"Arial Unicode MS-.  2 a_ller.-"Arial Unicode MS-. *2 ae(ETH), Bart Jacobs (KU .-"Arial Unicode MS-. 2 d Leuven) and .-"Arial Unicode MS-.  2 d%Bor.-"Arial Unicode MS-.  2 d+-.-"Arial Unicode MS-.  2 d,Yuh.-"Arial Unicode MS-. *2 d3Evan Chung (Berkley) . .-"Arial Unicode MS-. C2 i(Slides based on a presentation of Peter .-"Arial Unicode MS-.  2 iPM.-"Arial Unicode MS-.  2 iSu.-"Arial Unicode MS-.  2 iUller.-"Arial Unicode MS-. $2 i\given at MSR 5/2006).-G Root EntrydO)-2EY: Current User5SummaryInformation(*\PowerPoint Document(      !"#$%&'()K+,-./0123459=;<I>@ABCDEHhJiLMNOPQRSTUVWXYZ[\]^_`abcdefg " !#$%')*+DocumentSummaryInformation8MsoDataStore -2EY-2EY2US4QVVPV==2-2EY-2EYItem ?՜.+,D՜.+,    JOn-screen ShowMicrosoft Corporation<d ArialArial Unicode MSCalibriSymbolScript MT BoldTimes New RomanDefault Design<Lecture 4 Towards a Verifying Compiler: Data Abstraction4Review: Verification of OO Programs with InvariantsData Abstraction using MethodsEncoding of Pure Methods(Problem 1: Inconsistent Specifications Problem 2: Weak PurityProblem 3: Frame Properties$Data Abstraction using Model Fields'Variant of Problem 3: Frame PropertiesValidity PrincipleDecoupling PrincipleMutable Dependent PrincipleThe Methodology in Action"Automatic Updates of Model Fields Soundness3Problem 1 Revisited: Inconsistent Specifications -Problem 2 Revisited: Restricted Weak Purity&Problem 3 Revisited: Frame PropertiesSummary  Fonts UsedDesign Template Slide Titles0_」schulteschultePublishing ?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~keywords" minOccurs="0" maxOccurs="1" type="xsd:string"/> This value indicates the number of saves or revisions. The application is responsible for updatins:ds="http://schemas.openxmlformats.org/officeDocument/2006/customXml"/>dO)Nyi@DocumentLibraryFormDocumentLibraryFormDocumentLibraryForm*\ ExpirationDatePublishingStartDate 2018-12-08T06:59:54Z2000-01-01T00:00:00Zcript MT BoldS` T0BPDTimes New Roman` T0 B . @n?" dd@  @@`` h`;'  X       - D1H       &1H1 *"     3      )/ ;,,+        0 3f3@ʚ;ʚ;<4dddd,#0,g4{d{dTk T0ppp@  <42d2d,O$0` )___PPT12 %0___PPT10 ``6___PPT9{?  O  !Pj;Lecture 4 Towards a Verifying Compiler: Data Abstraction< <$ < | Wolfram Schulte Microsoft Research Formal Methods 2006 Purity, Model fields, Inconsistency _____________ 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) . Slides based on a presentation of Peter Mller given at MSR 5/2006 ^ Z Z Z Z(&4"J " I)"$  k     '  $  B   f3Review: Verification of OO Programs with Invariants44$ 4 nWhat were the 2 major tricks to support invariants? Which programs can we verify? What are the limitations? >4 :3 : o jData Abstraction using Methods  (Needed for Subtyping Information hiding 4 Z$ZZ)X     kEncoding of Pure Methods  ZPure methods are encoded as functions Functions are axiomatized based on specifications&7    l'Problem 1: Inconsistent Specifications  ( mProblem 2: Weak Purity  eWeak purity can be observed through reference equality How to prevent tests for reference equality? 2e8-3 f nProblem 3: Frame Properties  gResult of pure methods depends on the heap How to relate invocations that refer to different heaps?,h.)33 h o#Data Abstraction using Model Fields $ tSpecification-only fields Value is determined by a mapping from concrete state Similar to parameterless pure methods>N      p&Variant of Problem 3: Frame Properties''$ '  Assignment might change model fields of client objects Analogous problem for subtypes How to synchronize values of model fields with concrete fields?f7`7 @8  I rValidity Principle4  tOnly model fields of valid objects have to satisfy their constraints Avoids inconsistencies due to invalid objectsZE. 3#3R   Decoupling Principle4   Decoupling: Model fields are not updated instantly when dependee fields are modified Values of model fields are stored in the heap Updated when object is being packed pUR3#33p  tMutable Dependent Principle@   mMutable Dependent: If a model field o.m depends on a field x.f, then o must be mutable whenever x is mutable Dn$)3f     0 vThe Methodology in Action@   w!Automatic Updates of Model Fields " x Soundness  Theorem: Proof sketch Object creation new: new object is initially mutable Field update X.f := E; Model fields of X: asserts X.inv = mutable Model fields of X s owners: mutable dependent principle unpack X: changes X.inv to mutable pack X: updates model fields of X    c      c Z[  #  V  / z2Problem 1 Revisited: Inconsistent Specifications  3 Witness requirement for non-recursive specifications Ownership for traversal of object structures Termination measures for recursive specs  ,    },Problem 2 Revisited: Restricted Weak Purity--$ - ~%Problem 3 Revisited: Frame Properties&&$ & Model field solution does not work for methods with parameters Caching of values not possible for runtime checking Mutable dependent principle too strict  Summary  Data abstraction is crucial to express functional correctness properties Verification methodology for model fields Supports subtyping Is modular and sound Key insight: model fields are reduced to ordinary fields with automatic updates Verification methodology for methods (not yet ready) Partial solution: encoding, weak purity, consistency Future work: frame properties based on effectsZsx5ds(P35d&|    /"#$%&'(*,./02568;rjRjXFRp1ng this value after each revision.