2.2 Significance of the problem to component-based software engineering

A great deal of work on development of formal methods for software engineering has been done, resulting in many powerful systems for specifying, verifying, and otherwise supporting the development of software. Nevertheless, formal methods have the reputation for being more trouble than they are worth. Programmers are not interested in learning the details of formalisms (aside from their programming languages, of course!), and wonder why they should bother, since the formalization of a problem is often as time consuming as writing a program for it. Proponents of formal methods have a number of replies to this objection, including observations about how the formalization process makes the programming process easier, or reduces maintenance time, communicates program intentions better, or enhances the reusability of software. Despite all these stated (and often demonstrated!) advantages, formal methods remain unpopular.

Another tack taken by proponents of formal methods is to admit that there is an inherent cost in producing formal descriptions, which may well be prohibitive in the context of programming a single system, but that designers of reusable software have a different dynamic, whereby the cost of formalizing a software component can be amortized over multiple use of the component. The formal description of the component can be used to index the component in a library (distinguishing it from other similar components), as well as providing confidence for the reuser that the component will in fact behave as expected, and that the expectations have been expressed and understood clearly.

In order for this argument to work, however, we must suppose that it is possible to construct highly reusable software components, and that it is possible to motivate their use in enough contexts to make this economy of scale work. A number of approaches (e.g., [WOS94]) to making this dream a reality can be found in the literature. This paper takes no position on the eventual possibility of such an industry; however, until such time as such an industry is realized, we will need a story about how formal methods can be used in its absence, if we are to reap the benefits of the work to date on formal methods.