Implementing dormal definitions: projects 3 (Greg Michaelson)
Tue, 8 Feb 1994 09:39:26 GMT

          From comp.compilers

Related articles
Implementing dormal definitions: projects 3 (1994-02-08)
| List of all articles for this month |

Newsgroups: comp.compilers
From: (Greg Michaelson)
Keywords: tools
Organization: Dept of Comp & Elec Engineering, Heriot-Watt University, Scotland
Date: Tue, 8 Feb 1994 09:39:26 GMT

Another collaborative European project: the VDM-SL toolset.
Greg Michaelson
Date: Tue, 08 Feb 1994 09:04:55 +0000 (GMT)
From: (Marcel Verhoef)
Organization: Technical University Delft

The institute of applied computer science IFAD at Odense, Denmark has
a toolset (compiler, interpreter, debugger) for the development of
VDM-SL specifications. All the tools used, are formally defined in VDM-SL
itself (syntax, abstract syntax, operational and static semantics) and
implemented in C++. I have worked on part of the toolset for my MSc
thesis and the general development approach taken was as follows:

1) specify the tool in a VDM-SL, beginning at a high level of abstraction
      and lowering the level of abstraction until you have a fully explicit
      formal definition of your program
2) test the specification with the debugger, develop a test-suite
      (the debugger can be used in on-line and batch mode)
3) implement the program (e.g. in C++)
4) re-use the test-suite to "validate" the program.

Of course, this is not a single-in-line operation, the power of this
approach is that you can re-iterate ideas by trying out specification
styles in an early stage with the debugging environment and taking
design decisions along the way.

Second advantage is that the coding in (e.g.) C++ is quite easy and the
time used on actually writing code is reduced *dramatically*. Actually,
much of this work could be automated (and what I hear is that IFAD is
going to built such a code-generator). I wrote a 2500 line specification
of a prototype staic semantics analysis tool (which took me 3 months to
complete, including testing) and I coded 7500 lines of C++ code in
less than one month, implementing the specification. This is including
the "learning"-curve (I had reasonable knowledge of VDM, but never
programmed anything big in C++). Although it was a price-to-win
approach (ever tried to complete your MSc in time?) comparable results
from industry are there. So, I would urge everyone interested in
implementing formal specifications to have a very close look at
what is going on in the Formal Methods world. There are several
companies with industry-proof toolsets available. Apart from IFAD
I can think of Adelard and BP research in GB and CRI in DK. You can
get info about the IFAD VDM toolbox by emailing,
I don't know about the others.

Good entry-points are the proceedings of the VDM and FME conferences
which are published as lecture notes in computer science by Springer.


Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.