pcg@hplb.hpl.hp.com (Patrick Goldsack) (03/12/91)
Here at Hewlett-Packard labs in Bristol, England, we have been working
on a dialect of VDM together with supporting tools and documentation,
including course and reference material.
These are currently in use here at labs and in various
divisions around the company on product developments.
The notation is essentially a small and regular VDM dialect (uses pre/post specification,
relational modelling of state, type invariants and so on) with certain
extensions notably polymorphism and a module system similar in concept to that
available in algebraic languages such as CLEAR.
The tools (an early version was demonstrated at VDM-90 in Kiel) consist of
- a serverised database for holding specification components
(allows distributed network transparent access to specifiations,
multiple documents with multiple references to a specification
component without textual copying, etc)
- a type checker which can deal with equally well with
* individual declarations (such as a single function) even
in the presence of free identifiers,
* complex module combinations
- document formatting tools which generate the latex source
for the specification components embedded in doucment source
- an emacs-based interface for the above
The notation and tools are designed to support the incremental development of
specifications (Z-style) using a VDM-like notation. Thus, for example,
individual functions or types may be developed incrementally in a
document embedded in textual descriptions. These may then be combined
in a module to create the final `closed' specification.
Having received some interest from third parties,
we are now considering making the notation and tools available to a wider
audience, both educational and industrial.
We are looking initially for a limited number of beta-test sites
for these tools amongst users of formal specification notations.
The only requirement from the beta-sites would be a report after some
agreed period (e.g. 6 months) on the tools and notation, their usability,
bugs and so on.
If you are interested in the tools, notation or documentation
could you please mail me letting me know
1) who you are
2) how you might use the tools/notation
3) if you are interested in becoming a beta-test site
for the tools or notation
or
if you are not interested in beta-test but would
be interested in the tools or notation in the longer-term
4) platforms on which the software would be required
Note that this software is a `labs prototype' not an HP product, hence support
would not be via normal HP channels, nor of the level expected for a product.
Support will be on an informal basis via e-mail/phone direct with us
with no guarantees or liability on our part - although it is generally
in our interest to fix bugs and carry out enhancements.
We hope that the beta sites would be sufficiently familiar with specification
notations such as Z and VDM that formal training would not be required.
A course might be arranged if necessary, but would have to be
charged for at an appropriate consultancy rate (the course material itself
is not part of the beta-release).
For the beta-release there would be no charge from HP, although we
do currently rely on one piece of third party software for which a small
license fee may have to be paid.
Patrick Goldsack
Software Engineering Laboratory
Hewlett-Packard Labs,
Filton Road,
Bristol,
UK
+44-272-799910 x24176
pcg@hplb.hpl.hp.co.uk
--
_____________________________________________
Patrick Goldsack
HP Labs