Abstract
This paper describes a strategy for using the information contained in formal specifications to enhance a compiler's ability to perform optimizations. Because specifications are simpler than code and because they abstract away irrelevant implementation details, a compiler with access to specifications can determine that an optimization is safe more often than compilers that analyze only code. Furthermore, formal specifications can be used to allow programmers to define new optimizations.
Our strategy has been implemented in a prototype compiler that incorporates theorem proving technology. The compiler identifies opportunities to perform conventional and programmer-defined optimizations.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
J. P. Banning. An efficient way to find the side effects of procedure calls and the aliases of variables. In POPL, pages 29–41. ACM, January 1979.
D. R. Chase, M. Wegman, and F. K. Zadeck. Analysis of pointers and structures. In PLDI, pages 296–310. ACM, June 1990.
J. Ferrante, K. J. Ottenstein, and J. D. Warren. The program dependence graph and its use in optimization. ACM TOPLAS, 9(3):319–349, July 1987.
R. W. Floyd. Assigning meanings to programs. In Proceedings of Symposia in Applied Mathematics, volume 19, pages 19–31. AMS, 1967.
S. Garland and J. Guttag. A guide to LP, The Larch Prover. TR 82, DEC Systems Research Center, Palo Alto, CA, December 1991.
R. Gupta. A fresh look at optimizing array bound checking. In PLDI, pages 272–282. ACM, June 1990.
J. Guttag, J. Horning (eds.), with S. Garland, K. Jones, A. Modet, and J. Wing. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.
A. Hisgen. Optimization of User-Defined Abstract Data Types: A Program Transformation Approach. PhD thesis, Carnegie-Mellon University, 1985.
N. D. Jones and S. S. Muchnick. Flow analysis and optimization of LISP-like structures. In Program Flow Analysis: Theory and Application, pages 102–131. Prentice-Hall, 1981.
J. R. Larus and P. N. Hilfinger. Detecting conflicts between structure accesses. In PLDI, pages 21–34. ACM, June 1988.
B. Liskov and J. Guttag. Abstraction and Specification in Program Development. MIT Press, Cambridge, Ma, 1986.
J. M. Lucassen. Types and effects: Towards the integration of functional and imperative programming. MIT/LCS/TR 408, August 1987.
A. Neirynck, P. Panangaden, and A. J. Demers. Computation of aliases and support sets. In POPL. ACM, 1987.
B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Global value numbers and redundant computations. In POPL. ACM, 1988.
W. L. Scherlis. Program improvement by internal specialization. In POPL, pages 41–49. ACM, 1981.
B. Steffen, J. Knoop, and O. Rüthing. Efficient code motion and an adaption to strength reduction. In TAPSOFT '91 (LNCS 494), pages 394–415. Springer-Verlag, April 1991.
M. T. Vandevoorde. Optimizing programs with partial specifications. In Proceedings of the 1992 Larch Workshop. Springer Verlag. To appear.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vandevoorde, M.T. (1993). Specifications can make programs run faster. In: Gaudel, M.C., Jouannaud, J.P. (eds) TAPSOFT'93: Theory and Practice of Software Development. CAAP 1993. Lecture Notes in Computer Science, vol 668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56610-4_66
Download citation
DOI: https://doi.org/10.1007/3-540-56610-4_66
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56610-6
Online ISBN: 978-3-540-47598-9
eBook Packages: Springer Book Archive