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