On tight performance specification of object-oriented software components

Most modern designs of a software component include two separate pieces: functionality specification and implementation. When the specification is formal, this separation permits verification of reusable software components to be modular-essential for verification to be local, scalable, and hence, practical. In this paper, we explain the role of a third piece-an implementation dependent, performance specification-for a component. Introduction of this piece permits performance (e.g., execution time bonus) specification to be expressive (tight) while leaving functionality specification fully abstract and verification to be modular