The validation of software specifications with respect to explicit and implicit user requirements is extremely difficult. To ease the validation task and to give users immediate feedback of the behavior of the future software it was suggested to make specifications executable. However, Hayes and Jones [Hayes, Jones 89] argue that executable specifications should be avoided because executability can restrict the expressiveness of specification languages, and can adversely affect implementations. In this paper I will argue for executable specifications by showing that non-executable formal specifications can be made executable on almost the same level of abstraction and without essentially changing their structure. No new algorithms have to be introduced to get executability. In many cases the combination of property-orientation and search results in specifications based on the generate-and-test approach. Furthermore, I will demonstrate that declarative specification languages allow to combine high expressiveness and executability. In more than one way specifications play a central role in software development. They define all required characteristics of the software to be implemented, and thus form the starting point of any software development process. Specifications are also an important means of communication between users and developers -they can even be contracts. As formalized expressions of the requirements, specifications stand at the borderline between informal and formal descriptions of an application area. To precisely and concisely define the required characteristics, specifications must be written in formal and highly expressive languages [Wing 90]. For an immediate reflection of the consequences of the specifications and for an early validation, it has been suggested that specifications should furthermore be executable [Agresti 86]. Hayes and Jones [Hayes, Jones 89] however, argue that the demands for high expressiveness and executability exclude each other, and that executable specifications should be avoided. In addition, they state that executable specifications can negatively affect implementations. They support their arguments by a detailed and exhaustive discussion of specification problems which in their opinion cannot adequately be handled by executable specification languages. For two reasons I dissent. First of all, I consider the lack of correctness of software the most serious problem of software development, and not -as Hayes and Jones -the possible lack of expressive power of specification languages. Since the correct behavior of the software is defined by the requirements, and since the specifications are the basis for software development, all means applicable should be available to validate the specifications with respect to explicit and implicit requirements. Executable specifications can be crucial for this because they allow -in addition to formal reasoning about the specification -immediate validation by execution, and they provide users and developers with the touchand-feel experience necessary to validate non-functional behavior, e.g. user interfaces. Excluding executability from specification languages means therefore depriving oneself of a powerful method for validation. Second -as I will show in this paper -high expressiveness and executability need not exclude each other if specifications are written in declarative languages.
In response to these concerns, REF replied that it is the issue of correctness which is the major challenge in software development and not the expressiveness of specification languages.
Specifications Are (Preferably) Executable
Softw. Eng. J.
Softw. Eng. J.
Computer Science