Using specialized procedures and specification-based analysis to reduce the runtime costs of modularity

ABSTRACT

Managing tradeoffs between program structure and program efficiency is one of the most difficult problems facing software engineers. Decomposing programs into abstractions simplifies the construction and maintenance of software and results in fewer errors. However, the introduction of these abstractions often introduces significant inefficiencies.This paper describes a strategy for eliminating many of these inefficiencies. It is based upon providing alternative implementations of the same abstraction, and using information contained in formal specifications to allow a compiler to choose the appropriate one. The strategy has been implemented in a prototype compiler that incorporates theorem proving technology.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: W. W. Bledsoe and M. Tyson. The UT Interactive Prover. ATP 17, University of Texas Mathematics Dept., May 1975.
• 3: David Evans , John Guttag , James Horning , Yang Meng Tan, LCLint: a tool for using specifications to check code, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.87-96, December 06-09, 1994, New Orleans, Louisiana, United States
• 4: R. W. Floyd. Assigning meanings to programs. In Proceedings of Symposia in Applied Mathematics, volume 19, pages 19-31. American Mathematical Society, 1967.
• 5: S. Garland and J. Guttag. A guide to LP, The Larch Prover. TR 82, DEC Systems Research Center, Palo Alto, CA, December 1991.
• 6: S. M. German. Verifying the absence of common runtime errors in computer programs. Technical Report CS-81-866, Stanford, June 1981.
• 7: S. Ghemawat. Disk management for object-oriented databases. In Third International Workshop on Object orientation in Operating Systems, pages 222-225. IEEE Computer Society, December 1993.
• 8: David Gries, Programming Methodology: A Collection of Articles by Members of IFIP WG 2.3, Springer-Verlag New York, Inc., Secaucus, NJ, 1978
• 9: Rajiv Gupta, A fresh look at optimizing array bound checking, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.272-282, June 1990, White Plains, New York, United States
• 10: John V. Guttag , James J. Horning, Larch: languages and tools for formal specification, Springer-Verlag New York, Inc., New York, NY, 1993
• 11: Andy Lawrence Hisgen, Optimization of user-defined abstract data types: a program transformation approach (compiler), 1985
• 12: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 13: C. A. R. Hoare. Proofs of correctness of data representations. Acts Informatica, 1(1):271-281, 1972.
• 14: B Liskov , E Moss , A Snyder , R Atkinson , J C. Schaffert , T Bloom , R Scheifler, CLU reference manual, Springer-Verlag New York, Inc., New York, NY, 1984
• 15: D. C. Luckham, F. W. von Henke, B. Krieg-Bruckner, and O. Owe. ANNA Reference Manual, volume 260 of Lecture Notes in Computer Science. Springer-Verlag, 1987.
• 16: John McHugh, Towards the Generation of Efficient Code from Verified Programs, University of Texas at Austin, Austin, TX, 1984
• 17: G. Nelson and D. Detlefs. Extended static checking. Private communication on work in progress at DEC Systems Research Center, 1994.
• 18: R. Sites. Proving that computer programs terminate cleanly. Technical Report CS-74-418, Stanford, 1974.
• 19: Mark T. Vandevoorde, Specifications Can Make Programs Run Faster, Proceedings of the International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.215-229, April 13-17, 1993
• 20: Mark T. Vandevoorde, Exploiting specifications to improve program performance, Massachusetts Institute of Technology, Cambridge, MA, 1993
• 21: J. M. Wing, A TWO-TIERED APPROACH TO SPECIFYING PROGRAMS, Massachusetts Institute of Technology, Cambridge, MA, 1983
• 22: K. A. Yelick, A GENERALIZED APPROACH TO EQUATIONAL UNIFICATION, Massachusetts Institute of Technology, Cambridge, MA, 1985

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

General Terms:
Theory

Keywords:
compilers, formal specifications, program modularity, program optimization, software interfaces