Section 8

Abstract Interpretation

Recall some stuff of interpretation.

  • To interpret a program, is to explain its meaning, to run it, to reduce it to some outputs. (1 + 1 => 2)
  • The meaning of a program, is formally defined by its semantics. In our settings, it is usually defined by its operational semantics. ('a' '+' 'b' => a+b)
  • The semantics of a program formalizes the set of all possible executions in all environments. It is usually called concrete semantics.

People face problems. We ask questions like "Will my program terminate under all possible executions?", "Will the program never reach some states?". Because the concreate semantics is actually an infinity object, we cannot possibly write a program to examine every execution path.

Here comes two things.

  • People care about not only the output of a program, but also some properties/aspects of the program.
  • People need something other than concreate semantics so that we can possibly examine a program.

So we have abstract interpretation.

  • It can be viewed as a partial interpretation of the program.
  • It gains some information of a program without fully computing the concreate semantics.
  • e.g. Type, range of values, pre-conditions, post-conditions, etc.
  • It is a kind of approximation of the original semantics.
  • Therefore it is not precise. (Concrete 1 vs Abstract int)
  • But it may turn out eaiser to compute

And static analysis lies in the area of abstract interpretation. It is a sound, finite, approximate calculation of the programs's concrate semantics.

  • Sound: it should be correct, be consistent with original concrete semantics.
  • Finite: Regardless of original program, the static analysis always terminates.
  • Approximate: Not precise. It computes only some aspects/properties of the program.

We have a lot of specific static analysis techniques

  • Type checking/inference: compute only type related information
  • Array index checking: compute interval information
  • Constant folding: compute value range information
  • ...

People use abstract interpretation theories to prove that the abstraction of a program is sound/finite, and use them to direct the development of abstraction techniques. Theories include how concrete semantics and abstractions are related, how different level of abstractions are related, soundness and completeness, etc.