Models and Interpretations: Formalizing Multiple Semantics
SOFTWARE OPTIONS INC CAMBRIDGE MA
Pagination or Media Count:
We often think of a program as having different meanings in different contexts. When inferring types, for example, a compiler computes an upper bound on the possible types of each expression during execution. These upper bounds can be thought of as an interpretation of the program. When writing numerical software a programmer sometimes reasons as if the program operated on mathematical real numbers but at other times reasons about numbers with only finite precision, two rather different interpretations. This paper defines formal notions of interpretation and model to provide a counterpart to our intuitive understanding of the meanings of a program. Briefly, an interpretation is an assignment of labels to program terms, subject to constraints imposed by a model. This formalization lets us reason rigorously about relationships between different meanings and provides a conceptual framework for designing algorithms for program analysis, transformation, and execution. We develop and motivate the details through the example of a model in which an interpretation is a programs interprocedural flow graph. We also briefly discuss several other models in which interpretations are computed as part of the transformation and compilation machinery of the E-L programming environment and language.
- Computer Programming and Software