ࡱ> )+$%*-O(@ / 0DArialKakupopta``/@T0"DArial Unicode MS`/@T0" DCalibriicode MS`/@T0"0DWingdingsode MS`/@T0@DHGPSoeiKakupoptai`/@T02PDSymbolKakupoptai`/@T0 B . @n?" dd@  @@`` 80 9;AI U      ghi - D1H         &1H1 *" 7  >?AD        )  0 f3@ʚ;ʚ;<4dddd,#0,g4\d\dh@T0ppp@  <42d2d,O$0` )___PPT12 %0___PPT10 ``6___PPT9{?  O  9KLecture 2 Towards a Verifying Compiler: Logic of Object oriented ProgramsL L$ L xWolfram Schulte Microsoft Research Formal Methods 2006 Objects, references, heaps, Subtyping and dynamic binding, Pre- and postconditions, method framing _______________ 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)  P Pd& "C "  /#        Y     '  $   ~fReview: Boogie PL  gReview Boogie PL  What components does Boogie PL have, and what does it not have? What is the purpose of assert, assume and havoc? What s the meaning of a procedure and its modifies clause? What do we need to translate an OO language into Boogie PL? & (  1a "Axiomatizing the Spec# Type System   On notation: We use the following C# class class C : object { object f = null; C(){} } to describe the result of the axiomatization. We use the function Tr (anslate) to translate Spec# statements into BoogiePL% Z% Z !E-t      &   30  Storage Model  Use Boogie s type ref to denote runtime object references A Heap maps object references and field names to values var Heap: [ref, name] any; // Heap : ref name any Allocatedness is represented as another field of the heap const allocated: name; Access to an instance field f declared in C is translated as Tr[[ x = o.f; ]] = Tr[[ o.f = x; ]] =:% 9 F ;  = 1 %9):=   s  D             92A3\x$Constructors and Non-Virtual Methods%%$ % .Tr [[C() {} ]] = proc C..ctor(this: ref); requires this != null '" typeof(this) <: C; modifies Heap; impl C..ctor(this: ref) { assume Heap[this, allocated] == true; //for constructors only assume Heap[this, C.f] == null; call System.Object..ctor(this); & }x  ? H^   %      "           :           Virtual Methods: Example   class Cell{ public int x; protected virtual void Set(int x) modifies this.*; ensures this.x == x; { this.x = x; } public void Inc(int x) modifies this.*; ensures this.x==old(this.x)+x; { this.Set(Get()+x); } }   3f3f '  3f    +      +           class BackupCell: Cell{ int b; protected override void Set(int x) ensures this.b == old(this.x); { this.b = this.x; base.Set(x); } P! 3 !3f                       zbBehavioral Subtyping  Behavioral Subtyping should guarantee substitutability Wherever an object of type T is expected an object of type S, where S<:T, should do without changing the program s behavior expressed in wp Sufficient conditions: Let M1 be a virtual method and M2 be its overridden method, then M2 can weaken M1 s precondition M2 can strengthen M1 s postcondition 7XF&3a3 3 33@      ]yVirtual Methods  xTranslate each method m declared in C into a proc m.C (this, & ) requires this != null '" typeof(this) <: C; & The precondition of the overriding method is inherited from the overridden method; additional postconditions are conjoined Translate calls of the form o.m() to the method on o s most specific static typev=33B3  #   i  -     MBMethod Framing   xFor sound verification we assume that every method modifies the heap Modifies clauses in Spec# express which locations (evaluated in the method s prestate) a method is allowed to modify Modifies clauses for an object o or array a have the form: o.f allows modification of o s f field o.* allows modification of all of o s fields a[k] allows modification of a s array location k a[*] allows modification of all of a s array locationsb$ $ G3fd3f;  \    -       7   {cMethod Framing   Let W denote all locations a method is allowed to modify The Boogie PL post condition for a Spec# modifies clause Tr [[W]] = ("o: ref, f: name :: old(Heap[o,allocated]) (o,f) old(W) old(Heap[o,f]) = Heap[o,f]) ($ 9% $ 93f8  /    t  $            $Virtual Methods: Example Translation%%$ % tSpec# protected virtual void Set(int x) modifies this.*; Boogie proc Cell.Set(this : Cell, x : int) requires this != null '" typeof(this) <: Cell; modifies Heap; ensures ("o:ref, f: name :: old(Heap[o,allocated]) o = this old(Heap[o,f]) = Heap[o,f]);xAPPPP 3f3f'- A   )      !   2     /      ^z Loop Framing  pLoops might change the heap. Let W denote the set of locations potentially changed by the loop For sound verification we havoc the heap. We add as loop invariant the assertion that fields not written to don t change Tr [[W]] = ("o : ref, f: name :: Heapentry[o,allocated] f W Heapentry[o,f] = Heapcurrent[o,f]) where Heapentry/current denote the entry/current incarnations of the Heap variable in the loop Z{% ZaZ"3f   $$(((( ((((((,,,,,,,,H,,              Q vSummary  AVerifying object-oriented programs requires to axiomatize the declaration environment to keep enough information around for verification decide on a storage model to model updates and framing translate the method bodies, paying particular attention to partiality of operations virtual dispatch method and loop frames /'3=C/'3= C B 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  (     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   N@?Rectangle 3075"^ ` @ Z F     N@?Rectangle 3076"^  @ |* C   _   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*^ ` @ *  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_ ?% u p* C    @ V1? Rectangle 82947"@XK  u @ Hiu?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 ) u RClick to edit Master text styles Second level Third level Fourth level Fifth level!    S  @ Vptu? Rectangle 82949z  u X C    @ N~u?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 ? u 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 ; |   D (  D D PRu? Rectangle 83969z%  u V B    D Pu? Rectangle 83970 ?% u X B    D V@u? Rectangle 83971z  u V B   q  D Vhu? 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 ;  0aN0 @(  `  # hd0e0e ?Shape 2049"hbPK!'[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!7od%Sdrs/shapexml.xmlU]O0}`u!P"@bT3uؙ¯߱@4i}׾NNbi]mSΤ\s<钔r̵᧓ϟNµ /o$qb)r؆<>itR{xQIGAPflffY]y"M /,KOz΁Ԉ듡I`|3bI^YkJr|U#ՐMdEۛ+`;y6GGltv"n*m>arB*ǏS&i$[0˃ igtD]rm| t9Z٣%~ɂ:] ϑp`,h0jaDZ j%?VB9?OJ~11 XmN#QPTKLOOcRig+0;{IS}nW+YtZ buKht l`AQ ,3نv_zob뵋7Hb=~/peM<-Gl\,Dtp?TN*,]1uG*{s,7NLai弭WqͣJZ{ +6x |:ͨYc(_(I1NHQV82\Fv`+fV%BqHțH/u%qU$K|>VSH½S <ctXQh|cYBtwwcDN~PK!q drs/downrev.xmlDk07؋Ju0؆5_Jm ~-ףn2`6HPX38(xkP2@Ò' Ձg`ps]BH_5R~j:;DX>xnIHiLDs~YPDG8>ݐ6cOccN1n4m%?nB- `?<NV= (PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!7od%Sdrs/shapexml.xmlPK-!q Bdrs/downrev.xmlPKW  d @  # T{d0e0e ?Shape 2050"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!? edrs/shapexml.xmlWn6?Yˎ$BE mca`DQjTIqHIh| i73O]VZW3)*ow'9O e̸6߮5 kKoȉ}2qiGNjOj4ItTSY`/ۥeUIr6LScWkj$Ýn!'C?La `i&jnפ嵵i-p6N\5R 4kJre|:^'gn6u7c_Qjʒx?r@l$!@ bd".&S<9~Qǰ(/=Yߖ,Sk}9Nӳ .쏞ǫ[2 f jD_@J+"AE]jhmC1[ YSz .^BMJu\ buƒ瘅ecAQ ,Kٖ8 o#ndy^{ ["Hoޮ^^;@y=!#_&z+ (nں?UG,Pg\o+< B v9oMU8H ^BW *(g-1e]oOHQ]T㌪p3V$~ՋTR y,K)[=m8cDe+I>Q:pH8{E=C~%YBYɎƮc(黨ўn׫~(܇ 0h O o{jE{{bx2okPK! drs/downrev.xmlD]K0Cx\:˨ˆ ] :?.m޵Y&z0<^X -C7i2{o,w2ߜ?JrMd]8%t/PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!? edrs/shapexml.xmlPK-! drs/downrev.xmlPK ` d @H  0޽h ? 33___PPT10i..f+D=' 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  c(  r  S Tܒ  `}     c $t   i   Source language (eg. Spec#) . !&     <B T  `BoogiePL      <F bq NFormulas    L  c $i L  c $     0Kba\ >      08O& LTranslate source language features using particular programming methodologyM M M    0`T   9Translate Boogie PL code using particular VC generation : : :    <,Xq  p(Intermediate language for verification) ) ) H  0޽h ?/@ 33___PPT10i.4Fg!+D=' d= @B +< 0aN0 $(  r  S ^d  `}  d r  S _d  ` d H  0޽h ? 3380___PPT10.'20aN0 U(    # L0e0e ?Shape 112641"_YPK!'[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!a!|<drs/shapexml.xmlUO0~%"6B8mcg[J}v4Mx>8gߝ}w?z~H*sq&0E9>8y)eεϟΛ5 eMΗ7YRM#5t5ylXNzѠwܫ|fLmfjYU $S4xxFx^g:br]@7],L&kC8ؚoL"?m?B4j#O8{5Y0kP=L}&B̾hsx5[`3uC~gGr~柔8s|@,d'(M ŧԈg-4Wv 4_F9/Pwj"G#LZaAp 6kK{J^{Y?uz6R;_v/5`ln0(۩ z Iu]jIK}p?p{41d&Yj,Jh;P^8aj'm[UalFSF~${BJUJ@{〉py U6~\j a#!one)m=T'*#$_BZpu#I?aB>FK)YBFD׌~PK!֯͢ drs/downrev.xmlDO0M7d"0*okNvocb|rqjrUF3v" BWd] 8cm` GgCL98l|ICHRKuL#t c mIc`QkaBb#R䟛o`_ɩ}}Nbo]^[ ^?|K+pƳzW[9XE_8@촷_2~PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!a!|<drs/shapexml.xmlPK-!֯͢ 6drs/downrev.xmlPKN `}   Mapping Spec# to BoogiePL &    @M   # 0e0e ?Shape 112642"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!+wdrs/shapexml.xmlXn6;Y/޵yH[(u\%*VM*I;NN,}>I?{X4{( 9Crƴ>jJ 8*E2g֑*Hj%248& Ze&4Il5w R!iB9r8h0&㤦J96SU4^/ 83M'c8xF07Ik|Y|k[[* ="3_?4ıvCA\7 qrUp{l{jZO2>&])^Pϯ(e2gOp{:xS*f,rt9їgtIQ>:'f-@3gsGFp&Uz6L  gfJ䭖 R9v͸Cdn-ԪQ*[')B@#XMf1gO!qU2~Y|e%g(iznAbA ucKuX&aU_rr2+G ɗc{¶ÁF()8Y\ܶvvp^VG`a9_օ@LT U" B]|^q:(?36tU8 dܗrkSAY=_/+Lni.lkw+}Rw18c ?ա 1u$ }%aGȫDYuxjP4ѕ#ju!]]ЙBPTL[@BO/q; Q- U,˟wR> f&H5W~d{u'8tw7 rϻ^\';Ov=V]ǵ $w|m3PK!P drs/downrev.xmlDK0|).e*^6m$ᚤMA| " >  0aN0  (  r  S Td |}  d   S Td  `_<$@0 d X  0` P H  0޽h ? 33___PPT10.mv+EDZ' d= @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  (    # 6H0e0e ?Shape 52225"`ZPK!'[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.xmlU]O;}`I  RTE }Fl㵷ghQVBK=c37FJremo TɖdՅN~u8kCrcAuCkr^m#EӘA6 2[ ϖ[xQdYv,.j[9#$s6Ctϐ3«rMV{֚xy Ze4Z8c/8'4A.: BM (wU%tl$x> ;_q@6uP[+ ./'-y(g>XH=b<9ɰ{V?xt"pk!U暖.[gr2rIC@ U Ƨd]G%zgnѧ]kZ-zXk a΢r6C+ /Zn"G#,V`lV-T;µ!>BWca8=/zj{i>I.+x\|(J!V 5>-<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!J-drs/shapexml.xmlZn6}/ Zd}/eH[X,Ѡ$*VM*E'v-~II[]ǹA!␜33$>8H hC.#._noN() 1JJE?^y/rk"T%3fPw\K DYwj^`0y?ʇږOCM8f٥D &,~ZI0p2PѴ(akw8!R!N wRk0,.g\s,.`rOY3Ty@[^6{'ki '59$!s>;yĽ+1''K &ం',=J2gyΞ%ͥª(ftdIIj<F3 ۨۧM+¾VcMq]吠+[ٵoazU8*31OwZ;c^FsZ86V8&^篿 $J$W;\ &Vj{˚@|jtkǿYfc e˓/#Ww<1tdf#Nݑ+Q2ȺMIeM"}俹Z6lV*q"3ׂ37U-M*)Hc;8L0~HlœG*vDcf'+D]XMXnDeF/ +9 .&Z͆_ +PK!B?&EFR\Ǡ~of=t0] r`6*<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.xmlU]O;}`I  RTE }Fl㵷ghQVBK=c37FJremo TɖdՅN~u8kCrcAuCkr^m#EӘA6 2[ ϖ[xQdYv,.j[9#$s6Ctϐ3«rMV{֚xy Ze4Z8c/8'4A.: BM (wU%tl$x> ;_q@6uP[+ ./'-y(g>XH=b<9ɰ{V?xt"pk!U暖.[gr2rIC@ U Ƨd]G%zgnѧ]kZ-zXk a΢r6C+ /Zn"G#,V`lV-T;µ!>BWca8=/zj{i>I.+x\|(J!V 5>-<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!J-drs/shapexml.xmlZn6}/ Zd}/eH[X,Ѡ$*VM*E'v-~II[]ǹA!␜33$>8H hC.#._noN() 1JJE?^y/rk"T%3fPw\K DYwj^`0y?ʇږOCM8f٥D &,~ZI0p2PѴ(akw8!R!N wRk0,.g\s,.`rOY3Ty@[^6{'ki '59$!s>;yĽ+1''K &ం',=J2gyΞ%ͥª(ftdIIj<F3 ۨۧM+¾VcMq]吠+[ٵoazU8*31OwZ;c^FsZ86V8&^篿 $J$W;\ &Vj{˚@|jtkǿYfc e˓/#Ww<1tdf#Nݑ+Q2ȺMIeM"}俹Z6lV*q"3ׂ37U-M*)Hc;8L0~HlœG*vDcf'+D]XMXnDeF/     0          @X  0ptX  0_ cm X  0FpY H  0޽h ? 33___PPT10i.=q@F+D=' d= @B ++  0aN0 p(  r  S dm  `}  m r  S m  ` m X  0 @PX  0 @P% X  0@P9$  <$m qy,$0 assert o `" null ; x := Heap[ o, C.f ] assert o `" null ; Heap[ o, C.f ] := x L   33333333@       H  0޽h ? 33___PPT10.l#+,DO' d= @B D ' = @BA?%,( < +O%,( < +DA' =%(D' =%(D' =A@BBBB0B%(D' =1:Bvisible*o3>+B#style.visibility<*%(+8+0+0 +!0aN0 2*(    # ?m0e0e ?Shape 54273"SMPK!'[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.xmlTj1}/^Kkx:$Lq>`~j!dRbj]y*jR8R<ΰ: Ḍ6Y=AXŭ7g+i?Eh*twx1𭊰4njɣJ?V;!EWB@}*py U~ۍ"U-78GB>$\ m= cĕ/Ӊ Z!܁Bf_ߨ:%Q7mCtPK!z drs/downrev.xmlDN0DHuQ; u$X6MvM ͜3Š;v"[k$DLeUkj 0(! b~y1Lٳ) 5g( 8UCd`0FWs<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.xmlWn7;~,6नP.ڈK$%K>Yh}~$WS 7@t!,!9}3]#VXWk.gB]?\q<uAnG 2yV@? Y^%ƙ3DTau$_42΃'m83^9`>,xyeaD9L7L-LrGxyC +5dg9?EV0WJOO$PRT7\<|Z#h.:sK̨Dժ$:aQ&U@.³-aiO)-.Eulz4O?=l V\I{8/7G<Px/9s-5+M,_oџ3ȹP'hx4V2*&t?윷:E8[ 2cR i)ć8 :Ҩ[(_IAqTu-e 8-2LFC*w:fE-aGtпIT(LoQ&6 DsNO :RJ) n< NT [~ބ yK?oPK!x drs/downrev.xmlDQK0C/m1ݴ9klnbtIo9w^5CjGԅ>\  ja:n+28K8}P iQ]i~V ADTZX|6ʼkaM~yٺYviOo_`>Lf!rwȹh@?PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!<~ drs/shapexml.xmlPK-!x drs/downrev.xmlPKp H$D0 m 2Tr[[x = new T()]] = {var o: ref; assume o != null '" typeof(o) == T; assume Heap[o, allocated] == false; Heap[o, allocated] := true; call T..ctor(o); } :             @H  0޽h ? 33___PPT10n.AqP "+ CDB' d= @B D' = @BA?%,( < +O%,( < +D4' =%(D' =%(D' =4@BBBB%(D' =1:Bvisible*o3>+B#style.visibility<*Gk%(+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 +PT!灝ed,ڤ[ +PK!B?&EFR\Ǡ~of=t0] r`6*<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! Pdrs/shapexml.xmlUn1}G,I^ HQ&^ok/zx T*@9g.9{kjjg 9|;B[!-8 i|7}C+kCrcgYP+PxZmo(omw0kr`vh%u{Q<:: ŊZ-j ޮs!d2sjto)=Lu=rEV{Vx9K)>fk,gӮDog 9MƓwa7$ؔ*߼rWU?:Rrt2>><(׻(ԧ &b.˭•/%D"wy!G 'tHP?j?it *z`sMKqfG q~9 &] §$m%fgn1 ]Z.z^^ujx_p& 7V!1a,VU[B!E~sN^{^]vY<=Dtp?SL=]oq_T .Xm`o̸2); 9 B:mEXkai{+n/\Yw~ґ65/ͤ{$&^M)h,[wUn3uɗ7ޭt刻QvEPZl)*#oyS$iدz)TxP(T|Ig=싮m9'OJ˒rrwSNPK! drs/downrev.xmlDJ@E0|3$RRvTvf~qyގ#=:!Z0 +#[]s8 >-Eg4rۛȤt}j2;&Q cQ8%]MV}blETV`u-1+ϯ9ݝ8w@<*>$J8XP7!,r9Lke.|@ǁPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-! Pdrs/shapexml.xmlPK-! =drs/downrev.xmlPKP `}  m eMethods $   @N  # m0e0e ?Shape 55301" 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!Jdrs/shapexml.xmlZmo:~_vS[^ Mht!q ñ3P_sۇiJFD>/~_mVr&TL-"=gցJ@j%"4pbd }_:W:/E.¶TV͢Sarp\ve缓C 6bbL ˒_\w)q QwJPWT:'4H~ j!nOK8sǫXiPYҦX2\sjjo8yeQTFܡe:/մHZ7uR p#~O ve*AD@J>|q3+Sܭ2KnF$磵xU+lOb6 PNDz(Mݱl5$ʕ4[z+>)GJ^|l/G>M q1BȠW<,8PgЃ2gsD֔::|g+a0(-h#EOf/_%ˌoS_8TC&e0 'ZHZ@Pvj~BWdGau"߻?duKh=#[͂ю"!vٍ2>0z~hO ?)"`Dj{;E޵joS5I푏FOMiqѹ/|Y,eG^ wրM)IET8 4mԜ7Xo0W,N,IR=q 9[Q@)}?bw}QI= ST2O#Vzq#ʲWPߪ wBG'Kn8҄]>ǺW!soF dƿ8RT™@BL n66V+@&+lUU>,Ln2.qsYsVƊ *mQ$ՎzZ eIˈ`֠4bIun.C?kĈF6)P9g$ 9Wm$uԵdmwZ%ܷ6 CX`trQszԦ ]GG PTq KJtꍭ689+5`D܉dKEs[¥~p!G,ui3]㡤l=qԈNZDzEjsu)*# pܡڻ:b8cc(*WM&\ߨ1tPK!18 drs/downrev.xmlDQO0M5Ÿ!e1i\@|z۵e/11>}gUKҺZ#("ТƒAxqF5,g3}T3_. *MB+*i#q*hK*,? nID48\TJM)&z Ҕ%Sb_}<|=g횝ɛf2`0~ikrePK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!Jdrs/shapexml.xmlPK-!18 drs/downrev.xmlPK @ mxp___PPT9RJ kRecall: Boogie PL has only procedures, no instance methods Add this as first parameter to generated proc is weakly typed (just int, bool, ref) Spec# types must be preserved via contracts has no idea of heap properties Allocatedness must be preserved via contracts has no inheritance Strengthening of postconditions must be implemented via multiple procedures$ Z) Z/ !Z& Z- !Z Z/ !Z ZL !Z)'&- /  LZ    S    @H  0޽h ? 33___PPT10i.Bq0+D=' w= @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 + ]'.J kJR +PK!B?&EFR\Ǡ~of=t0] r`6*c dR ?=s`=1E/t2f9`d#rb`Ҁ*K,: \iPm4ш'R& SQ,#c^hhPLTnP|~Dٟd FtrAو nFe`b$$eyNJ1k%R$ VX3PLFL.MX ϻx62n6Rj El.p[Rƭq@S#  滏U +4޻NeC\\dDиA%B*i%O܌F#]f w5slGU!j/f2vIU ]،>2-ϖ3Ùn>0}> W>*7^/WhK?m).-NKD{b.ϱyW]YG6_7,F6?r8Wx Ŧ6Q Q乴fWj7oſ jhg܀FVuhi,Z7v.OZGCэט ղym˩\C=֗r4@;1EUeٚPK-!B<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!0m35drs/shapexml.xmlUMo1W|B D RJ(B!9W6xm]򥪪K氌=3yo>r~HJ3=p&0y2~w}tƙsRFˌk/Ɵ?ש|K/$qb)+rǦ؊pf_ko4^M8c=tXDec{N,m[o%V҂؋дUh/\T1ʰ4nf)*?Q;!EWR@s*py U~ۋ"U/78GB޼$B m=-cĕV/ w IBw ڕ" ~~4 5FR3bcu?JB3J/PK!7#] drs/downrev.xmlD[K@C8ov-Q4^m=Mbv&.87l1.:uV # JV ^5Ds%x2PӓOUP. MJ܍A mM}`ˎ\R Uao`鞈x5]~$+;?<?gXxvYv/Cn&+WXVy (PK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-!0m35drs/shapexml.xmlPK-!7#] 3drs/downrev.xmlPKJ `}  d  @L  $ # u0e0e ?Shape 70658"R L 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.xmlWn8 x]eDZ(E FaD9I5EjIʱsoOt(ZM0Hΐ|:~$[ cKb{LL祚3@ 1W9q=5ýN/'ZBЦS3FX8v JO0JꙡQa53c~9SPjhi;_dm>pr7[V}5蛅2h%4M8So8_|Q4>lg<>Z룆ɺ0DˇQ Q41X;}E!9d}Px3'n}Qn ?h8:isٍӀɿR= (‰yhI8ye TadMURgv0%n#ClnKT3yT٥GB\ʱ|b~9ǂ墸4mI#\#`s;[RD3Vj͸ra֨ /aM"W l2VLXwxƽiv}G_kMsSW8 :Y/+}2ߝ6ګ6 ݰ bB8HyorfBiamTe.Ta̅:`D=Hg7B3ҷď8[ zFzQ⒢F*[OIAYR7Ѻc[s)CIEJ_RŠղi+.?8KܖfZݲ cRCfw %v+p'C^d"ՏF)vz^&3JwS=(dSZs/GO#'޶W>'PSg@| |¿/O,Ѣ|˦ֵo׻Ļe}VKO0 +QhjI0* gu. KIzcp0Jqrb]tDTFg,r&qF&V)GaPL 2Hnb2X2l rCހԭq.pdGS{%6 nnuR[c^c?Bl]Y)dvZi,v'Lml/ ŷ[6 ]AB \x$Qv b9ȗmY>6lq\iꗒ= V2ΣNPK-!'[Content_Types].xmlPK-!1_a _rels/.relsPK-! !drs/shapexml.xmlPK-! *drs/downrev.xmlPKA H @H $ 0޽h ? 33___PPT10i.H`+D=' w= @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 +N qrv-VKC +PK!B?&EFR\Ǡ~of=t0] r`6*rcz f~"Xl 1Oh+'0L hp    (00Towards a Verifying Compiler The Spec# Approachschulteschulte194Microsoft Office PowerPoint@p=@r2@v.(\Gg   9  y--$xx--'"Arial Unicode MS-.  2 q1."System-"Arial Unicode MS-. 3f2 @ Lecture 2.-"Arial Unicode MS-. 3f32 #Towards a Verifying Compiler:.-"Arial Unicode MS-. 3f92 ,!Logic of Object oriented Programs.-"Arial Unicode MS-. 2 :BWolfram Schulte.-"Arial Unicode MS-. "2 ?@Microsoft Research.-"Arial Unicode MS-. $2 D;Formal Methods 2006.-"Arial Unicode MS-. 12 Q:Objects, references, heaps, .-"Arial Unicode MS-. 2 T: Subtypingc.-"Arial Unicode MS-. '2 TLand dynamic binding, .-"Arial Unicode MS-.  2 X3Pre.-"Arial Unicode MS-.  2 X9-.-"Arial Unicode MS-.  2 X;and .-"Arial Unicode MS-. 2 XBpostconditions.-"Arial Unicode MS-. 2 XY, method framing.-"Arial Unicode MS-. 2 f_______________g.-"Arial Unicode MS-. 2 jJoint work with .-"Arial Unicode MS-. .2 j%Rustan Leino, Mike Barnett.-"Arial Unicode MS-. 2 jK , Manuel k.-"Arial Unicode MS-.  2 jXF.-"Arial Unicode MS-.  2 jZa.-"Arial Unicode MS-. 2 j\hndrich.-"Arial Unicode MS-. '2 jf, Herman Venter, Rob .-"Arial Unicode MS-. 2 jDeLine.-"Arial Unicode MS-.  2 j, .-"Arial Unicode MS-. 62 mWolfram Schulte (all MSR), and .-"Arial Unicode MS-. 2 m=Peter .-"Arial Unicode MS-.  2 mEM.-"Arial Unicode MS-.  2 mHu.-"Arial Unicode MS-.  2 mJller.-"Arial Unicode MS-. 2 mO(ETH), .-"Arial Unicode MS-. 2 mY Bart Jacobs.-"Arial Unicode MS-. 2 mj(KU Leuven) and .-"Arial Unicode MS-.  2 mBor.-"Arial Unicode MS-.  2 m-.-"Arial Unicode MS-.  2 mYuh.-"Arial Unicode MS-. 2 mEvan ,.-"Arial Unicode MS-. 2 pChung (Berkley) .-PropertiesDIJYUQWC4PQ==2 ~EY ~EYItem  PropertiesPQK2NU0ZGJEFQ==2 ~EY ~EYItem "Properties$ <_ schulteschulte  !"#$%&'()*+,-./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 updatistoreItem ds:itemID="{A458516E-9138-42CD-A3BA-00CA8B4B6356}" xmlns:ds="http://schemas.openxmlformats.org/officeDocument/2006/customXml"/>w> PublishingStartDateRoot EntrydO) ~EY, Current UserSummaryInformation(|PowerPoint Document(4      & !"#'10/-.(  !#%&'՜.+,D՜.+,T    On-screen ShowMicrosoft Corporation4 d ArialArial Unicode MSCalibri WingdingsHGPSoeiKakupoptaiSymbolDefault DesignLLecture 2 Towards a Verifying Compiler: Logic of Object oriented ProgramsReview: Boogie PLReview Boogie PLMapping Spec# to BoogiePL#Axiomatizing the Spec# Type System#Axiomatizing the Spec# Type System#Axiomatizing C# Type DeclarationsStorage Model AllocationMethods%Constructors and Non-Virtual MethodsVirtual Methods: ExampleBehavioral SubtypingVirtual MethodsMethod FramingMethod Framing%Virtual Methods: Example Translation Loop FramingSummary  Fonts UsedDesign Template Slide Titles0PublishingExpirationDateDocumentLibraryFormDocumentLibraryFormDocumentLibraryForm ng this value after each revision.