DOC PREVIEW
Berkeley COMPSCI 164 - Lecture Notes

This preview shows page 1 out of 2 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 2 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 2 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Lecture #41: Topics in Static Analysis: Program VerificationSpecificationsSpecifying a LanguageMore Obvious StuffSequencesIf StatementsAssignment StatementsPitfallsLecture #41: Topics in Static Analysis: ProgramVerification• Previously looked atstatic analysis, finding properties of programsthat don’t depend on the specific input data.• So far, have seen:– Static type checking (are these types consistent?)– Type inference (what must the type of this be?)– Analyses for optimization (what assignment statements might lasthave set x’s value?)• These have all used simple and fast algorithms.• Today’s example of more ambitious analysis:program verificationtries to determine if a program does what it is specified to do.Last modified: Tue May 3 19:10:51 2005 CS164: Lecture #41 1Specifications• Starting in the 1960’s, resea rchers started asking what it meant to“prove” a program.• First need a statement of what a program does.• Obvious approach: notate a program withassertions:{ P } S { Q }where P and Q are logical asser ti ons and S is some program text.• P is aprecondition, and Q is apostcondition.• Above meansIf P is true, S is execute d, and S terminates normally, then Qwill be true.• Simple Example:{ k > 0 ∧ x ≤ y } x = x-k { x < y }Last modified: Tue May 3 19:10:51 2005 CS164: Lecture #41 2Specifying a Language• To prove “program a ssertions” like this, must first come up withaxioms for the dynamic semantics of the language.• One (older, but moderately intuitive) style due to C.A.R. Hoare.• Start with something easy: For any predicate P ,{P } pass {P }Last modified: Tue May 3 19:10:51 2005 CS164: Lecture #41 3More Obvious Stuff• Logically entailed assertions may replace other assertions.P ⇒ R, {R}S{Q}{P }S{Q}• The line means “to prove the thing below, show the things on top.”Last modified: Tue May 3 19:10:51 2005 CS164: Lecture #41 4Sequences• To concatenate two statements:{P }S1{R}, {R}S2{Q}{P }S1; S2 {Q}Last modified: Tue May 3 19:10:51 2005 CS164: Lecture #41 5If Statements• Problem: want to demonstrate that{ P }if C :S1else:S2{ Q }• Assume that conditional expression C has no side effects.• So break into two cases:{ P ∧ C } S1 { Q }{ P ∧ not C } S2 { Q }and prove both.• What would case without else look like? Change S2 rule toP ∧ not C ⇒ Q.• What would case with elifs look like? Add rules such as{P ∧ not C1 ∧ not C2 · · · ∧ Cn} Sn {Q}Last modified: Tue May 3 19:10:51 2005 CS164: Lecture #41 6Assignment Statements• A bit tricky. We’ll consider scalar variables only.• First, some terminology. If P is a logical assertion, define P [x → E]mean “P with all free insta nces of x replaced by E.• For example (x > y)[x ← 3] is 3 > y.• Now we can write a “backward rule” for assignment:{P ⇒ Q[x ← E]}{P } x = E {Q}• Example: to show{ i > 0 ∧ xn= yxi} y = y*x { i > 0 ∧ xn= yxi−1}Last modified: Tue May 3 19:10:51 2005 CS164: Lecture #41 7Pitfalls• Consider our first example:{ k > 0 ∧ x ≤ y } x = x-k { x < y }Problem: It’s not valid! Suppose that (mathematically) x − k < −231.• The construct x-k is a “false friend”—it onlylookslike the mathe-matical expression x − k, but means something slightly different.• Could sprinkle all our specifications with additional clauses checkingfor this, but things quickly become unwieldy.• So generally, we punt in some way:– say that we have proved “modulo overflow”– or prove the property separately.• Another example: a postcon di ti on on a sorting routine that says sim-ply “the array A is sorted.” So is this OK?def sort (A): for i i n range (0, len (A)): A[i] = iIn general, how do we know our specification is sufficient?Last modified: Tue May 3 19:10:51 2005 CS164: Lecture #41


View Full Document

Berkeley COMPSCI 164 - Lecture Notes

Documents in this Course
Lecture 8

Lecture 8

40 pages

Load more
Download Lecture Notes
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Lecture Notes and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Lecture Notes 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?