Two-level semantics and abstract interpretation

AbstractTwo-level semantics is a variant of Scott/Strachey denotational semantics in which the concept of binding time is treated explicitly. This is done by formally distinguishing between those computations that take place at run-time and those that take place at compile-time.Abstract interpretation is concerned with the (preferably automatic) analysis of programs. The main purpose of these analyses is to find information that may assist in the efficient implementation of the programs. Abstract interpretation is thus related to data flow analysis, partial evaluation and other program analysis methods. Its unique flavour is the insistence on formal proofs of correctness and the methods used to establish these.This paper develops a theory of abstract interpretation for two-level denotational definitions. There are three ingredients in this. First a framework for proving the correctness of analyses is developed. This may also be used to compare the precision of various analyses. Next it is shown that, given a choice of properties of programs, one may specify a most precise analysis (or best induced analysis). This may also be used to investigate the collecting semantics (or static semantics). Finally, we show how to modify the most precise analysis in order to obtain an implementable analysis where we trade off precision for implementability.The impact of this theoretical development is that for a large class of programming languages the semantic considerations of correctness and precision come for free by applications of metaresults: it merely suffices to define the analyses, the meaning of the properties studied and to prove the correctness of the language-dependent primitives. The theory then guarantees the correctness of the analyses for all programs. This success is one of the successes needed in order to develop efficient and provably correct implementations directly from semantic definitions