Lecture #41: Topics in Static Analysis: Program VerificationSpecificationsSpecifying a LanguageMore Obvious StuffSequencesIf StatementsAssignment StatementsPitfallsLecture #41: Topics in Static Analysis: ProgramVerification• Previously looked atstatic a nalysis, 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 assign ment statements might lasthave set x’s value?)• These have all used simple and fast algorithms .• Today’s example of more ambiti ous analysis:program verificationtries to determine if a program does what it is specifie d to do.Last modified: Tue May 3 19:10:5 1 2005 CS164: Lecture #41 1Specifications• Starting in the 1 9 60’s, researchers started asking wh a t it meant to“prove” a progra m.• First need a statement of what a program does.• Obvious approach: notate a program w i thassertions:{ P } S { Q }where P and Q are logical asserti ons and S is some progr a m text.• P is aprecondition, and Q is apostcondition.• Above meansIf P is tr ue , S is executed, and S terminates normall y, then Qwill be true.• Simple Example:{ k > 0 ∧ x ≤ y } x = x-k { x < y }Last modified: Tue May 3 19:10:5 1 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 } pas s {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 expres sion 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?• What would case with elifs look like?Last modified: Tue May 3 19:10:51 2005 CS164: Lecture #41 6If Statements• Problem: want to demonstrate that{ P }if C:S1else:S2{ Q }• Assume that conditional expres sion 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?Last modified: Tue May 3 19:10:51 2005 CS164: Lecture #41 6If Statements• Problem: want to demonstrate that{ P }if C:S1else:S2{ Q }• Assume that conditional expres sion 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 instances of x replaced by E.• For example (x > y)[x ← 3] is 3 > y.• Now we can write a “backward rule” for a ssignment:{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 (mathema ti ca l l y) x − k < −231.• The construct x-k is a “false friend”—it onlylookslike the mathe-matical expression x − k, but means some thing sl i g htly diffe rent.• Could sprinkle all our specifications with additiona l clauses checkingfor this, but things quickly become unwieldy.• So generall y, we punt in some way:– s a y that w e have proved “modulo overflow”– or prove the proper ty separately.• Another example: a postcondition on a sorting routine that says sim-ply “the array A is sorted.” So is this OK?def sort (A): for i in r ange (0, len (A)): A[i] = iIn general, how do we know our specifica ti on is sufficient?Last modified: Tue May 3 19:10:51 2005 CS164: Lecture #41
View Full Document
Unlocking...