3 The Human Factor

  In general, a specification should be clear, concise, and unambiguous. It must be decidable whether a given implementation fulfills a certain specification, and whether a specification reveals enough, for the corresponding components to be used intelligently. Overspecification, lack of orthogonality, and ambiguities should be easily detectable.

Formal methods provide ways to check these requirements. For this, a specification language should be based on a formal semantics. This does not, however, imply that it has to use a very symbolic mathematical notation.

Specification formalisms are often optimized for expressiveness and brevity, leading to symbolic notations which are not easily readable for the average programmer. Many specification techniques dictate a functional style of thinking, whereas most programmers are more accustomed to the imperative paradigm. Likeness to programming languages flattens the learning curve and improves acceptance. The difficulties and the number of errors increase with the extent of the transformation between the way the we think and the paradigm and notation in which we express our thoughts. This is not to say that we should not be exposed to different paradigms and notations to broaden our horizons. But in reality, changing the way we think is very difficult. In this paper we concentrate on components implemented in imperative programming languages. We do not address the specification of components written in functional or logic programming languages and the integration of components using different paradigms.

Specifications must not only be easy to write, but also to read. Component specifications are read by many people with different backgrounds.

The lack of tool support degrades specifications to mere documentation. The inclination to write a specification which can be executed/simulated and which can serve as a rapid prototype is higher than to write a mere documentation specification. Additionally, if tool support provides for refinement proofs between different versions of a specification and between specifications and implementations the usefulness of specifications and their usage increase. We have experienced ourselves that students, who could not be motivated to write a single specification using pencil and paper, spent days writing B specifications [Abr96,BC95], because the latter can be simulated and provide a base for machine-assisted correctness proofs of their implementations. The symbolic notation and the lack of tool support are the key factors why formal semantic contracts are the most important non-practice in component software.