Nothing Special   »   [go: up one dir, main page]

skip to main content
article
Open access

ACE: an automatic complexity evaluator

Published: 01 April 1988 Publication History

Abstract

There has been a great deal of research done on the evaluation of the complexity of particular algorithms; little effort, however, has been devoted to the mechanization of this evaluation. The ACE (Automatic Complexity Evaluator) system is able to analyze reasonably large programs, like sorting programs, in a fully mechanical way. A time-complexity function is derived from the initial functional program. This function is transformed into its nonrecursive equivalent according to MacCarthy's recursion induction principle, using a predefined library of recursive definitions. As the complexity is not a decidable property, this transformation will not be possible in all cases. The richer the predefined library is, the more likely the system is to succeed. The operations performed by ACE are described and the use of the system is illustrated with the analysis of a sorting algorithm. Related works and further improvements are discussed in the conclusion.

References

[1]
AHO, A. V., HOPCROFT, J. E., AND ULLMAN, J. D. The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, Mass., 1974.
[2]
BACKUS, J.W. Can programming be liberated from the Von Neumann style? A functional style and its algebra of programs. Commun. ACM 21, 8 (Aug. 1978), 613-641.
[3]
BACKUS, J.W. The algebra of functional programs: function level reasoning, linear equations, and extended definitions. Lecture Notes in Computer Science, 27. Springer-Verlag, New York, 1981, 1-43.
[4]
BURSTALL, R. M., AND DARLINGTON, J. A transformation system for developing recursive programs. J. ACM 24, 1 (Jan. 1977), 44-67.
[5]
COHEN, J. Computer-assisted microanalysis of programs. Commun. ACM 25, 10 (Oct. 1982), 724-733.
[6]
DARLINGTON, J., AND BURSTALL, R.M. A system which automatically improves programs. Acta Inf. 6, 1 (1976), 41-60.
[7]
DARLINGTON, J. Program transformation. In Functional Programming and Its Applications. J. Darlington, P. Henderson, and D. Turner, Eds. Cambridge University Press, 1982.
[8]
FEATHER, M.S. A system for assisting program transformation, ACM Trans. Program. Lang. Syst. 4, 1 (Jan. 1982), 1-20.
[9]
GUTTAG, J. V., HORNINO, J., AND WILLIAMS, J. FP with data abstraction and strong typing. In Proceedings of 1981 Conference on Functional Programming, Languages, and Computer Architecture (Portsmouth, 1981). ACM, New York, 1981, 11-24.
[10]
KNUTH, D. E. The Art of Computer Programming. Addison-Wesley, Reading, Mass., 1973.
[11]
LE M~TAYER, D. Analysis of functional programs by program transformation. In Proceedings of 1987 France-Japan Artificial Intelligence and Computer Science Symposium (Cannes, 1987). North-Holland, Amsterdam.
[12]
MACCARTHY, J. A basis for a mathematical theory of computation. In Computer Programming and Formal Systems. P. Braffort, and D. Hirsberg, Eds. North-Holland, Amsterdam, 1963.
[13]
MANNA, Z., NESS, S., AND VUILLEMIN, J. Inductive methods for proving properties of programs. Commun. ACM 16, 8 (Aug. 1973), 491-502.
[14]
STANAT, n. F., AND MACALLISTER, D.F. Discrete Mathematics in Computer Science. Prentice- Hall, Englewood Cliffs, N.J., 1977.
[15]
WEGBREIT, B. Mechanical program analysis. Commun. ACM 18, 9 (Sept. 1975), 528-539.
[16]
WEGBREIT, B. Goal-directed program transformation. IEEE Trans. Softw. Eng. SE-2, 2 (June 1976), 69-80.
[17]
WILLIAMS, J. On the development of the algebra of functional programs. ACM Trans. Program. Lang. Syst. 4, 4 (Oct. 82), 733-757.

Cited By

View all
  • (2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
  • (2023)A Class of Programs that Admit Exact Complexity Analysis via Newton?s Polynomial InterpolationProceedings of the XXVII Brazilian Symposium on Programming Languages10.1145/3624309.3624311(50-55)Online publication date: 25-Sep-2023
  • (2022)Modeling Asymptotic Complexity Using ACL2Electronic Proceedings in Theoretical Computer Science10.4204/EPTCS.359.9359(83-98)Online publication date: 24-May-2022
  • Show More Cited By

Recommendations

Reviews

D. John Cooke

The ACE system provides a partial procedure for finding the worst-case complexity of FP programs. The notion of complexity used is essentially the (order of magnitude of the) number of recursive calls necessary for the program evaluation; as such, the complexity is expressed as a composite of standard functions such as exponentials and logarithms. Having such a measure facilitates comparison of different equivalent programs such as might be obtained by a program transformation system. This is paradoxical because ACE uses the FP algebra to perform transformations and simplifications of Cf, the complexity function for the program under investigation ( Cf is derived by a straightforward syntax-directed translation from the given FP program, f). Subsequently, recursion induction is used to extract a nonrecursive function. Other topics that the reader will encounter include fixpoint theory, folding, computational induction, and the splitting of complex conditionals into a set of simpler forms that each involve a single condition (following McCarthy). Unfortunately, as complexity is inexorably related to termination and termination is undecidable, the system does not always successfully yield a complexity function for a given program. Adding more transformations, more information on `standard' functions, and better approximating functions extends the set of programs on which ACE will succeed. The addition of more rules within the system, however, makes the rule selection process harder and the system slower—but that's another problem. The paper flows well; it consists of two introductory sections, two technical sections, a sizable example (example 3 of section 5 includes illustrations of most of the technical points mentioned earlier), and a conclusion. There is little comparable material in the literature, but all related background is adequately cross-referenced for those who need to brush up on their theory. The ACE system, emanating from ESPRIT project 302 (funded by the EEC), is a very neat application of established theory that is used to harness the emerging technology of program transformation. The use of the FP algebra is central to the methodology, but extensions to other similar languages are clearly possible by using FP as an internal/intermediate form. There are a few bothersome typographical errors and other minor irritations (most notably `verify' for `satisfy,' lower case `o' for the function composition symbol 3:9D, and :3WCfor the atom that is the empty sequence rather than &fgr; as used by Backus in his original FP paper) but all in all this is a very readable paper describing interesting and useful work.

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems
ACM Transactions on Programming Languages and Systems  Volume 10, Issue 2
April 1988
154 pages
ISSN:0164-0925
EISSN:1558-4593
DOI:10.1145/42190
Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 1988
Published in TOPLAS Volume 10, Issue 2

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)88
  • Downloads (Last 6 weeks)11
Reflects downloads up to 10 Nov 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
  • (2023)A Class of Programs that Admit Exact Complexity Analysis via Newton?s Polynomial InterpolationProceedings of the XXVII Brazilian Symposium on Programming Languages10.1145/3624309.3624311(50-55)Online publication date: 25-Sep-2023
  • (2022)Modeling Asymptotic Complexity Using ACL2Electronic Proceedings in Theoretical Computer Science10.4204/EPTCS.359.9359(83-98)Online publication date: 24-May-2022
  • (2022)Denotational semantics as a foundation for cost recurrence extraction for functional languagesJournal of Functional Programming10.1017/S095679682200003X32Online publication date: 5-Jul-2022
  • (2021)An Inversion Tool for Conditional Term Rewriting Systems - A Case Study of Ackermann InversionElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.341.3341(33-41)Online publication date: 6-Sep-2021
  • (2021)Mechanisation of the AKS AlgorithmJournal of Automated Reasoning10.1007/s10817-020-09563-y65:2(205-256)Online publication date: 1-Feb-2021
  • (2020)Denotational recurrence extraction for amortized analysisProceedings of the ACM on Programming Languages10.1145/34089794:ICFP(1-29)Online publication date: 3-Aug-2020
  • (2019)Isolation Modeling and Analysis Based on MobilityACM Transactions on Software Engineering and Methodology10.1145/330660628:2(1-31)Online publication date: 26-Feb-2019
  • (2019)Amortized Complexity VerifiedJournal of Automated Reasoning10.1007/s10817-018-9459-362:3(367-391)Online publication date: 1-Mar-2019
  • (2019)Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time CreditsJournal of Automated Reasoning10.1007/s10817-017-9431-762:3(331-365)Online publication date: 1-Mar-2019
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media