Advanced Topics in Computer Graphics
Advanced Topics in Computer Graphics CMPS 290
Popular in Course
Popular in ComputerScienence
This 33 page Class Notes was uploaded by Dr. Elyssa Ratke on Monday September 7, 2015. The Class Notes belongs to CMPS 290 at University of California - Santa Cruz taught by Staff in Fall. Since its upload, it has received 33 views. For similar materials see /class/182267/cmps-290-university-of-california-santa-cruz in ComputerScienence at University of California - Santa Cruz.
Reviews for Advanced Topics in Computer Graphics
Report this Material
What is Karma?
Karma is the currency of StudySoup.
Date Created: 09/07/15
Theorem Proving 10 Feb 2004 290G Lecture 11 1 34 Theorem Proving HisTorical PerspecTive Theorem proving or auTomaTed deducTion logical deducTion performed by machine AT The i nTersecTion of several areas MaThemaTics original moTivaTion and Techniques Logic The framework and The meTareasoning Techniques One of The mosT advanced and Technically deep fields of compuTer science Some resulTs as much as 75 years old AuTomaTion efforTs are abouT 40 years old 10 Feb 2004 290G Lecture 11 2 34 Applications Hardware and software verification or debugging Automatic program synthesis from specifications Discovery of proofs of conjectures A conjecture of Tarski was proved by machine 1996 There are effective geometry theorem provers 10 Feb 2004 290G Lecture 11 3 34 Program Verification Fact mechanical verification of software would improve software productivity reliability efficiency Fact such systems are still in experimental stage After 40 years Research has revealed formidable obstacles Many believe that program verification is extremely difficult 10 Feb 2004 290G Lecture 11 4 34 Program Verification FacT VerificaTion is done wiTh respecT To a specificaTion Is The specificaTion simpler Than The program 9 WhaT if The specificaTion is noT righT 9 Answem Developing specificaTions is hard STill redundancy exposes many bugs as inconsisTencies We are inTeresTed in parTial specificaTions An index is wiThin bounds a lock is released 10 Feb 2004 290G Lecture 11 5 34 Theorem Proving and Software Semantics Meets specFound Bug Speci cation V ge e Validi C n ration Provability theorem proving Theorem in a logic Sound ness If the theorem is valid then the program meets specification If the theorem is provable then it is valid 10 Feb 2004 290G Lecture 11 6 34 Theorem Proving Program Analysis STarT from real code and face headon issues like aliasing and sideeffecfs looping daTa Types and recursion excepTions MosT ofTen used for sequenTial programs Ambi rious Modes r Complex properTies Simple properTies Flow sensiTive Flow insensi39live Inter procedurd Infraprocedural Semiau roma ric AuTomaTic Reguires invarian rs and Discovers simple invarian rs validaTes Them Theorem Proving Type SysTems STarT from real code and face headon issues like aliasing and sideeffecTs looping daTa Types and recursion excepTions Mosle for sequenTial programs and some concurrenT AmbiTious Fairly ModesT Complex properTies fairly Verify Type properTies where arbiTrary predicaTes over sTaTe lOOPS GlIGSCS CXCCPlIOHS CTC d0 space noT cause big problems Flow sensiTive Flow insensiTive InTerprocedural 39 IIquot LerquotPrquot3Cedl39r C l SemiauTomaTic SemiauTomaTic Reguires invarianTs and Reguires invarianTs and validaTes Them validaTes Them 10 Feb 2004 290G Lecture 11 8 34 Overview of The Next Few Lectures Focus Expose basic fheorem proving fechm39ques usefu for soffware debugging From programs To Theorems VerificoTion condiTion generoTion From Theorems ro proofs Theorem provers Decision procedures Applications 10 Feb 2004 290G Lecture 11 9 34 Programs Theorems Axiomafic Semantics Consis rs of A language for wriTing specificaTions abouT programs Rules for es rablishing when specifica rions hold Typical specifica rions During The execu rion only nonnull poinTers are dereferenced This program Termina res wi rh x 0 Par rial vs ro ral correc rness specifica rions Safe ry vs liveness proper ries Usually focus on safe ry par rial correc rness 10 Feb 2004 290G Lecture 11 1034 Specification Languages MUST be easy To use and expressive conflic ring needs Mos r of ren only expressive Typically They are ex rensions of rstorder logic AlThough higherorder or modal logics are also used We focus here on s ra rebased specifica rions safe ry S ra re values of variables conTenTs of heap pasT sTaTe NOT allowed variable x is livequot lock L will be releasedquot I There is no correla rion beTween The values of x and yquot 10 Feb 2004 290G Lecture 11 11 34 A Specification Language We39ll use a fragmen r of rstorder logic Formulas P A True I false I P1 P2 P1 P2 AP VxP AToms A E1 E2 E1 E2 fA1An All boolean expressions from our language are aToms Can have an arbi rrary collec rion of predica re symbols reachableE1E2 lisT cell E2 is reachable from E1 sorTeda L H array 0 is sorTed beTween L and H p rrET expression E deno res a poin rer To T E pTrT same in a differenT noTaTion An asser rion can hold or no r in a given s ra re Equivalenle an asserTion denoTes a seT of sTaTes 10 Feb 2004 290G Lecture 11 1234 Hoore Triples PorTioI correcTness P s Q When you sTorT s in any sToTe ThoT soTisfies P If The execuTion of s TerminoTes IT does so in o sToTe ThoT soTisfies Q ToToI correcTness P s Q When you sTorT s in any sToTe ThoT soTisfies P The execuTion of s TerminoTes and IT does so in o sToTe ThoT soTisfies Q Defined i nducTiver on The sTrucTure of sToTemenTs 10 Feb 2004 290G Lecture 11 13 34 Home Rules P 51 Q Q 52 R P 51 32 R P1 31 P2 52 E P1K4 E P2 ifE rhenslelseszQ IKEsI IK4EQ I whileEdosQ 10 Feb 2004 290G Lecture 11 1434 Hoare Rules Assignment Example P x x 2 x gt 5 Wha r is P General rule QUEX X E Q Surprising how simple The rule is The key is To compu re quotbackwardsquot The precondi rion from The pos rcondi rion Before Hoare P x E x39 Px39x K x Ex39x 10 Feb 2004 290G Lecture 11 15 34 Home Rules Examples Wha risPin P xxyx0 m yo y0 Px5 xy10 10 Feb 2004 290G Lecture 11 1634 Home Rules Assignment Bu rnow rr39y Px5 xy10 P ough r To be y 5 or39 x y The Home rule would give us x y 105x 5 y 10 y 5 we Ios r one case How come The rule does no r work 10 Feb 2004 290G Lecture 11 1734 Home Rules Assignment Bu rnow rr39y Px5 xy12 P ough r To be y 7 and x yquot The Home rule would give us x y 125x 5 y 12 y 7 wrong How come The rule does no r work 10 Feb 2004 290G Lecture 11 1834 Handling Program TaTe Hoare rules assume absence of aliases BuT real programs have aliases ImporTanT Technique 1 Model The sTaTe of heap as a symbolic mapping from addresses To values If E denoTes an address and p a heap sTaTe Then sepE denoTes The conTenTs of memory cell updpEV denoTes a new heap sTaTe obTained from p by wriTing V aT address E 10 Feb 2004 290G Lecture 11 1934 More on Memory We allow variables To range over39 heap s ra res So we can quanTify over39 all possible heap sTaTes And we use The special pseudovariable p in asser rions ro r39efer39 To The current s ra re of The heap Example Vi i 2 O i lt 5 gt seii A i gt Oquot allposi rivep A O 5 says ThaT enTries O4 in array A are posiTive 10 Feb 2004 290G Lecture 11 2034 Home Rules SideEffects To cor39r39ec rly model wr39i res we use memory expressions A memory wr39i re changes The value of memory QUPdH E1 E2H E1 E2 Q Reason Ia rer39 abou r memor39y expressions wi rh infer39ence rules such as McCarthy E2 E1 2 E3 5 UPdHI E1 E2 E3 2 56K E if E i E 3 1 3 10 Feb 2004 290G Lecture 11 21 34 Memory Aliasing Consider again A x 5 x y 10 We ob rain A x y 10uPdM x 5m sent x selm y 10 updm x 5m selupda x 5 x selupda x 5 y 10 5 selupda x 5 y 10 ifxyThen55 10ese5seay 10 xyor39y5 To is Theorem genera rion Fr39om ro is Theorem proving 10 Feb 2004 290G Lecture 11 2234 Memory Aliasing Consider again A x 5 x y 12 We obTain A x y 12uPdM x 5m sent x selm y 12 updm x 5m selupda x 5 x selupda x 5 y 12 5 selupda x 5 y 12 ifxyThen55 12ese5seay 12 if x y Then false else 5 sela y 12 xyand y7 To is Theorem generaTion From To is Theorem proving 10 Feb 2004 290G Lecture 11 23 34 Alternative Handling for Memory Reasoning abou r aliasing can be expensive NPhard Some rimes comple reness is sacrificed wi rh The following approxima re rule E2 E1ObViOUSIY E3 seupdul E1 E2 E3 36K E3 E1 ObViOUSIY E3 o rherwise p is a fresh p new parame rer The meaning of obvious varies The addresses of Two disfinc r globals are 7t The address of a global and one of a local are i PREfix and GCC use such schemes 10 Feb 2004 290G Lecture 11 2434 Home Rules Examples Consider x2 xx1 xlt5 xlt2 xx1 xlt5 xlt4 xx1 xlt5 They all have cor39r39ec r pr39econdi rions Bu r The Ios r one is The mos r general or weakesf pr39econdi rion 10 Feb 2004 290G Lecture 11 25 34 Dijksfm39s Weakest Preconditions ConsiderP s Q Predica res form a Ia r rice false 1 True sTrong T T Weak weakesT P precondi rion WPs Q Tover39ify P S Q compu re WPs Q and grove P 1 WPs Q 10 Feb 2004 290G Lecture 11 2634 Weakest Preconditions Compu red by a backward reading of Hoare r39ules P 51 Q Q 52 R P 51 32 R quot WP51 52 R WP31 WP52 R 10 Feb 2004 290G Lecture 11 2734 Weakest Preconditions Compu red by a backward reading of Hoare r39ules QUEX gtlt E Q 39 WPgtlt E Q QEgtlt 10 Feb 2004 290G Lecture 11 2834 Weakest Preconditions Compu red by a backward reading of Hoare r39ules P1 31 P2 52 E i P1K4 E i P2 ifE rhenslelseszQ wpif E Then 31 else 32 Q E i Wp31QK 4 E i wpsz Q 10 Feb 2004 290G Lecture 11 2934 Weakest Preconditions Exercises WP y xl xy 2 WP if xy Then x x else x y xy 9 WP while xgt0 do x xO 9 10 Feb 2004 290G Lecture 11 3034 Weakesf Preconditions Cont Whaf abouf loops Define a family of WPs WPkwhile E do 5 Q weakesf precondifion on which i The loop ferminafes in k or fewer iferafions if ferminafes in Q WP0 4 E f Q WP1 E f WPs WP0 K 4 E f Q WPwhiIe E do 5 B Kk 0 WP Kind of hard To compufe Can we find somefhing easier yef sufficienf 9 10 Feb 2004 290G Lecture 11 31 34 Not Quite Weakest Preconditions Recall what we are trying to do false 1 True strong T T weak weakest P precondition WPs Q verification condition VCs Q We shall construct a verification condition VCs Q require loops annotated with loop invariants VC is guaranteed stronger than WP But hopefully still weaker than P P t VCs Q t WPs Q 10 Feb 2004 290G Lecture 11 3234 Verification Condition Generation Computed in a manner similar to WP Except the rule for while VCwhileI E do 3 Q I K 5x1xn I t E VCs I K 4 E t Q I holds I 393 PreserYed 39 Q holds when the on entry 0 My 39TemT39On loop terminates I is the loop invariant provided externally x1 xn are all the variables modified in s The 5 is similar to the 5 in mathematical induction PO K 5n N Pn Pn1 10 Feb 2004 290G Lecture 11 33 34