Surely the very suggestion that formal specs can be translated into anything
is heresy, unless you're working with an executable subset. Oh, you
can always call it constructive refinement: there's a new project looking
at this at the University of Essex. There was also some work on translating
VDM into Prolog at the University of Manchester some years ago, I think by
Ian Cottam. Jim Murray, now at Napier University, built an SML toolkit for
executing Z specifications which is described in a Heriot-Watt MSc
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
