Specifications can make programs run faster

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.