What’s the difference between a type system and an abstract interpretation? When would you want to use one over the other?
Could you give an example of a type system that could prevent division-by-zero errors?
Say you have a language of integer expressions. Define the concrete and abstract domains for a sign analysis on this language.
in is given by a state value given to the concrete interpreter.
Draw the lattice for this abstract domain.
Write the abstraction and concretization functions for this abstract interpretation.
Describe the relationship between and ; what property must hold?
Define the abstract interpretation for this language for literals and in.
What should the abstract interpretation of the following expressions be?
State the soundness property with respect to and/or .
If the first expression resulted in , would this be sound?
If the second expression resulted in , would this be sound?
How could you use this analysis to tell if an expression will definitely divide by 0?
How could you use this analysis to tell if an expression may divide by 0?
Are there any cases where this analysis is not complete—i.e., it says there is a potential (“may”) divide by 0, but dividing by 0 is actually impossible?
How could you ameliorate this?
Board
Notes
Think aloud! Even if I’m lost, talking through my thinking is critical.
Partial evaluation: this is the term for anything where we partially evaluate a program at compile time.
