### Create a StudySoup account

#### Be part of our community, it's free to join!

Already have a StudySoup account? Login here

# Advanced Topics in Computer Graphics CMPS 290

UCSC

GPA 4.0

### View Full Document

## 33

## 0

## 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.

## Popular in ComputerScienence

## Reviews for Advanced Topics in Computer Graphics

### What is Karma?

#### Karma is the currency of StudySoup.

#### You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!

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

### BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.

### You're already Subscribed!

Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'

## Why people love StudySoup

#### "Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."

#### "I made $350 in just two days after posting my first study guide."

#### "Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."

#### "It's a great way for students to improve their educational experience and it seemed like a product that everybody wants, so all the people participating are winning."

### Refund Policy

#### STUDYSOUP CANCELLATION POLICY

All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email support@studysoup.com

#### STUDYSOUP REFUND POLICY

StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here: support@studysoup.com

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to support@studysoup.com

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.