This thesis describes an implementation of abstract interpretation and its application to strictness analysis and termination analysis. The abstract interpretation is performed based on a lattice-theoretical model of abstraction, or translation, of functions expressed in a lambda-calculus notation and defined over a concrete domain into functions defined over a user-specified, application-dependent, abstract domain. The functions thus obtained are then analyzed in order to find their least fixed-points in the lattice which is the abstract domain, using a method which is a simplification of the frontiers algorithm of Chris Clack and Simon Peyton Jones. In order to achieve the required efficiency, this method is implemented using lattice annotation, along with constraints upon the annotations. The implementation is then applied to the problems of strictness analysis and termination analysis, deriving useful pre-compilation information for many functions. The concrete domains over which the functions are defined may or may not include lists. / Science, Faculty of / Computer Science, Department of / Graduate
| Identifer | oai:union.ndltd.org:UBC/oai:circle.library.ubc.ca:2429/28354 |
| Date | January 1988 |
| Creators | Westcott, Doug |
| Publisher | University of British Columbia |
| Source Sets | University of British Columbia |
| Language | English |
| Detected Language | English |
| Type | Text, Thesis/Dissertation |
| Rights | For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use. |
Page generated in 0.0025 seconds