I. Introduction A. Who B. what is program analysis? ------------------------------------------ WHAT IS PROGRAM ANALYSIS? Def: *program analysis* is predicting statically safe approximations to the set of configurations or behaviors that may occur dynamically. ------------------------------------------ C. why study program analysis (course spec) ------------------------------------------ WHY PROGRAM ANALYSIS? Automatic understanding of programs is - important + optimizing compilers + program development tools + formal verification: - safety critical systems - business critical systems + research in programming languages - impossible, in general + safe approximations Basic ideas: - compute abstractions - use in transformations Goals: - little or no input from programmers ==> practical, usable - correctness ==> usable "under the covers" - efficient (at compile time): - time - space ------------------------------------------ 1. useful ideas ------------------------------------------ MAIN IDEAS OR THEMES - conservatism: "Err on the safe side!" - efficiency from approximation: "Trade precision for efficiency!" ------------------------------------------ What's an example of the first idea from type checking? Suppose we're interested in numerical precision (error estimation), what's an example of the second idea in this case? 2. practicality 3. widely used 4. it's new for me what about the material interests you? D. Plan of course (syllabus) Would you make any changes to the plan? E. Objectives 1. meta What kind of questions should you be asking? 2. normal ------------------------------------------ OBJECTIVES - Explain the goals of program analysis, how it can be used, as well as its advantages, disadvantages, and limits. - Judge and improve the quality of various kinds of program analyses. - Explain and generalize the mathematical ideas that are used in various program analysis techniques. - Apply program analysis techniques to calculate various properties of small programs. - Use and explain operational semantic descriptions of programming languages. - Prove the soundness of an analysis with respect to the operational semantics of a language. ------------------------------------------ F. How I'll run the course 1. overview 2. red tape G. summary any other questions about the course? II. Semantics Overview A. Semantic description techniques what does a denotational semantics tell you about a statement? an operational semantics? an axiomatic semantics? --------------------- { x >= 3 } x := x + 1 { x > 3 } --------------------- --------------------- (x >= 3) = wp.(x := x+1).(x > 3) --------------------- B. remark about models, presentations, and theories What's the theory that a denotational semantics constructs a model for?