|Implementing dormal definitions: projects 3 email@example.com (1994-02-08)|
|From:||firstname.lastname@example.org (Greg Michaelson)|
|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.
Date: Tue, 08 Feb 1994 09:04:55 +0000 (GMT)
From: email@example.com (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 firstname.lastname@example.org,
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.
Return to the
Search the comp.compilers archives again.