comp.software-eng archive file "blurb/specbox" last changed 31 Jul 1993 This file contains information on the following subjects. Numbers in column 1 count distinct messages with the corresponding subject. 1 SpecBox: a formal methods tool for VDM ------------------------------------------------------------------------ From: pkdf@dcs.ed.ac.uk (Peter Froome) Subject: SpecBox: a formal methods tool for VDM Date: 24 Jul 92 15:21:52 GMT Organization: Laboratory for the Foundations of Computer Science, Edinburgh U SPECBOX VERSION 2.21 ____________________ A new version of Adelard's formal specification support tool for draft BSI/ISO VDM has now been released. The new version has several improvements and enhancements over older versions, including the following: * A revised grammar, reflecting the latest draft standard * An improved LaTeX facility * An improved, much faster, semantic analyser * An interface to the Mural proof assistant Prices now run from 495 to 1995 UK pounds for single user supported licences, with academic site licences between 250 and 500 UK pounds. DESCRIPTION SpecBox is an industrialised tool for inputting, checking and printing VDM specifications. It is composed of four main parts: * A syntax checker * A LaTeX generator * A semantic analyser * A Mural translator The syntax checker is used to input specifications in the ASCII form of BSI/ISO VDM and check them for grammatical errors. The checker comprises an editor linked to a parser; it gives help on the valid VDM terms to enter at each stage, and also enables the grammar to be investigated and particular syntactic classes to be chosen. It also completes phrases (by closing brackets, for example) automatically. The LaTeX generator produces a source file for the LaTeX document preparation system that will print the specification in the mathematical syntax. Line numbering, cross-references and subscripts are supported. The semantic analyser carries out checks on the well-formedness of the specification. These checks include matters such as declaration, scope, number of arguments, use of state variables and hooked values, use of record types and constructor functions, and use of 'is- expressions'. The semantic analyser displays diagnostic messages while it is running, and on completion produces a report file, an annotated listing and a cross-reference table. The algorithm used for analysis prevents many redundant cascade error messages from being generated after the first occurrence of a semantic problem. The Mural interface enables specifications produced using SpecBox to be transmitted to the Mural proof assistant for the generation and discharge of proof obligations. (Mural was developed by Manchester University and the Rutherford Appleton Laboratory.) SpecBox is continually being enhanced: future developments include * A version for Microsoft Windows 3.1 * Mathematical syntax support * Full support for BSI/ISO VDM modules Existing customers receive upgrades at preferential prices. For further information contact: Peter Froome Adelard Coborn House 3 Coborn Road London E3 2DA UK Tel: +44 (0)81 983 0214 Fax: +44 (0)81 983 1845 Email: pkdf@dcs.ed.ac.uk