On Mon, 20 Oct 1997, Greg Michaelson wrote:
...
> dissertation. But you should look at the Jones and Hayes paper from Software
> Engineering Journal called something like "Executions are not (always)
> executable" to discover why persons of good taste in the formal community
> will no longer speak to you if you take this any further...
>
> Greg Michaelson
>
Whilst not wanting to get embroiled into a formal methods argument,
the two extremes of this debate are represented by the Jones and Hayes
paper cited above (SEJ 4(6), 1989) and the follow-up article by Fuchs
("Specifications are (preferably) executable", SEJ Sept. 92).
In practice the benefits of being able to execute a specification
have to be weighed against the drawback of biasing a specification
towards a particular algorithm. One of the most popular and effective
commercial formal methods tools (the IFAD VDM-SL toolbox; see
http://www.ifad.dk) allows (amongst other things) interactive debugging
of specifications with breakpoints. This has proved extremely effective
in capturing errors in the specification which would have proved costly
to remedy at later stages of the design cycle.
Paul.
====================================================================
Dr Paul Mukherjee | email: [EMAIL PROTECTED]
School of Computer Studies | tel: 0113 233 5193
University of Leeds | fax: 0113 233 5468
Leeds LS2 9JT. | WWW: www.scs.leeds.ac.uk/paulm/
====================================================================
