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