A Formal Approach to Software Component Specification
Kung-Kiu Lau, Mario Ornaghi · 2001
There is a general consensus that the paradigm shift to component-based software development should be accompanied by a corresponding paradigm shift in the underlying approach to specification and reasoning. Work in modular specification and verification has shown the way, and following its lead, in this position paper, we outline our approach to specifying and reasoning about components, which uses a novel notion of correctness. 1 What is this paper about? As the title suggests, this paper is about an approach to formal specification of software components. The purpose of such an approach is to allow formal reasoning about components. The ultimate goal of Component-based Software Development (CBD) is third-party assembly. To achieve this, it is necessary to be able to specify components in such a way that we can reason about their construction and composition, and correctness thereof, a priori. Work in modular specification and verification, e.g. [9, 14] has shown the way, and our approach follows its lead. However, our approach is novel and hence different in the way we define correctness. In this paper, we will discuss how we specify components, and in particular how we define and reason about correctness, and why this is useful for CBD. 2 Specifying Components Ideally components should be black boxes, in order that users can (re)use them without knowing the details of their innards. In other words, the interface of a component should provide all the information that users need. Moreover, this information should be the only information that they need. Consequently, the interface of a component should be the