The validation of specifications with respect to user requirements is extremely difficult. To ease the validation task and to give users immediate feedback on the behaviour of the future software, it was suggested that specifications should be made executable. However, Hayes and Jones 1 argue that executable specifications should be avoided because executability can restrict the expressiveness of specification langugages, and can adversely affect implementations. We 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. Furthermore, we show that declarative specification languages combine high expressiveness and executability.
展开▼
