Executing Formal Specifications need not be Harmful

We review the various arguments which have been advanced for and against the use of executable specifications. Examples are given of the problems which 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. We conclude 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