On Static Properties of Specialized Programs

Specializing programs by partial evaluation is well defined extensionally, but in practice no intensional properties, such as what the specialized programs will look like or how they will run, can be ensured. We propose a technique for obtaining information about the intensional properties of specialized programs based only on the partial evaluator and the source program. This is useful, e.g., when the static data are not yet available, when we specialize with respect to a large number of static data and want to predict the quality of the results, or when we wish to state formal results about the family of residual programs obtained by specializing the same source program. The approach is based on a self-applicable polyvariant specializer and uses a grammarng abstract interpretation. This paper reports ongoing research, and the grammar-generating interpretation is only developed and proven safe for a subset of the target language. The remaining parts are outlined, but not completed. ...

• Type: Conference
• Year: 1991
• Where: SAS
• Authors: Karoline Malmkjær
• Keywords: Formal Methods, Intensional Properties, SAS 1991, Source Program, Specialized Programs