Executing formal specifications need not be harmful

The various arguments that have been advanced for and against the use of executable specifications are reviewed. Examples are provided of the problems that may arise in applying this technique and of the benefits which may accrue. A case study is reported in which execution is used to validate the published specification of a commercially available package. It is concluded that there are circumstances when executable specifications can be of high value but that execution must be used together with, and as a supplement to, other methods of validating specifications such as inspection and proof