Specifications are (preferably) executable

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 I.J. Hayes and C.B. Jones (1989) argue that executable specifications should be avoided because executability can restrict the expressiveness of specification languages, and can adversely affect implementations. The author argues 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, he shows that declarative specification languages combine high expressiveness and executability