Implementing dormal definitions: projects 3

Another collaborative European project: the VDM-SL toolset.
Greg Michaelson
----------------------------------------------------------------------
Date: Tue, 08 Feb 1994 09:04:55 +0000 (GMT)
From: marcel@dutct05.tudelft.nl (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 toolbox@ifad.dk,
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 comp.compilers page.
Search the comp.compilers archives again.