D. Le Metayer
Abstract
There has been a great deal of research done which investigates the problem of evaluating the complexity of particular algorithms; little effort however has been applied to the mechanization of this evaluation. This paper presents the ACE (for Automatic Complexity Evaluator) system which is able to analyse reasonably large programs like sorting programs or numerical programs in a fully mechanical way. A complexity function is derived from the initial program. This function is then automatically transformed into its non-recursive equivalent according to MacCarthy's recursion induction principle, using a pre-defined library of recursive definitions (for example id, length, exponential ...). As the execution time is not a decidable property, this transformation will not be possible in all cases. The richer the pre-defined library is, the more likely the system is to succeed. The paper presents the reasons for mechanizing complexity calculus and the problems involved. It describes the operations performed by ACE and its implementation; limitations and further improvements are discussed in conclusion.
- 1 Backus J., Can programming be liberated from the Von Neumann style? A functional style and its algebra of programs. Comm. ACM, Vol. 21, 8 (August 78), pp. 613-641. Google Scholar
Digital Library
- 2 Cohen J., Zuckerman C., Two languages for estimating program efficiency. Comm. ACM, Vol. 17, 6 (June 74), pp. 301-308. Google ScholarDigital Library
- 3 Gordon M., Milner R., Wadsworth C., Edinburgh LCF. Springer-Verlag (1979).Google Scholar
- 4 Guttag J. V., Horning J., Williams J., FP with data abstraction and strong typing. Proc. of the 1981 Conf. on Functional Programming Languages and Computer Architecture (October 81), pp. 11-24. Google ScholarDigital Library
- 5 MacCarthy J., A basis for a mathematical theory of computation. Computer Programming and formal systems (1963).Google Scholar
- 6 Wegbreit B., Mechanical program analysis. Comm. ACM, Vol. 18, 9 (September 75), pp. 528-539. Google ScholarDigital Library
- 7 Wegbreit B., Goal-directed program transformation. IEEE Trans. on Software Engineering, Vol. SE-2, 2 (June 76), pp. 69-80. Google ScholarDigital Library
Index Terms
- Mechanical analysis of program complexity
Recommendations
Mechanical analysis of program complexity
SLIPE '85: Proceedings of the ACM SIGPLAN 85 symposium on Language issues in programming environmentsThere has been a great deal of research done which investigates the problem of evaluating the complexity of particular algorithms; little effort however has been applied to the mechanization of this evaluation. This paper presents the ACE (for Automatic ...
Point-free Program Transformation
Program Transformation: Theoretical Foundations and Basic Techniques. Part 1Functional programs are particularly well suited to formal manipulation by equational reasoning. In particular, it is straightforward to use calculational methods for program transformation. Well-known transformation techniques, like tupling or the ...
Proving Theorems by Program Transformation
To Andrzej Skowron on His 70th BirthdayIn this paper we present an overview of the unfold/fold proof method, a method for proving theorems about programs, based on program transformation. As a metalanguage for specifying programs and program properties we adopt constraint logic programming ...
Comments