Abstract Interpretation
Point: Abstract interpretation of programs is a unified approach to apparently unrelated program analysis techniques.
Syntax
- Program: a set of "nodes".
- Node: has successor and predecessor nodes
- Entry: no pred, one succ
- Assignment: one pred, one succ; "Ident" <- "Expr"
- Test: one pred, two succ; if "Bexpr" then "Expr" else "Expr"
- Junction: one succ, more than one pred.
- Exit: one pred, no succ.
Semantics
- $S_0 = lattice(S \,\cup {\bot_S, \top_S}), \forall x \in S, \bot_S \leq x \leq \top_S$
- "Values" semantic domain: a complete lattice as sum of primitive domains
- $Env = Ident^0 \rightarrow Values$
- Meaning of an expression: $val: Expr \rightarrow [Env \rightarrow Values]$, in particular $\underline{val}: Bexpr \rightarrow [Env \rightarrow Bool]$
- $\forall s \in States, s = \langle cs(s), env(s)\rangle$, i.e. control state and environment state
- ??? if $e \in Env, v \in Values, x \in Ident$, then $e [v / x] = \lambda y . \underline{cond}(y = x, v, e(y))$
- $\texttt{n-state }: States \rightarrow States$
And there are a lot of other stuff defined. But in total they look pretty puzzling to me ...
Static Semantics of Programs
$Cv$ is a static summary of the possible executions of the program.
Before that, a lot of definitions are here. But I hardly know the motivations for such definitions.
Quite difficult. I decide to have a glimpse at MIT course first.
Note of Notes of MIT Course
Well .. The first slide is a bit puzzling ... I should continue or look at the reading assignments? CONTINUE.
This paper reading will be transformed into course reading of the MIT course.