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

1 December 1994

proceedings article
Published by Association for Computing Machinery (ACM)

Vol. 19 (5) , 121-127
https://doi.org/10.1145/193173.195300

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.

Keywords

This publication has 6 references indexed in Scilit:

Disk management for object-oriented databases
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
LCLint
Published by Association for Computing Machinery (ACM) ,1994
A fresh look at optimizing array bound checking
Published by Association for Computing Machinery (ACM) ,1990
ANNA A Language for Annotating Ada Programs
Published by Springer Nature ,1987
Proof of correctness of data representations
Acta Informatica, 1972
An axiomatic basis for computer programming
Communications of the ACM, 1969