🚀 go-pugleaf

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