home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #16 / NN_1992_16.iso / spool / comp / software / 2949 < prev    next >
Encoding:
Internet Message Format  |  1992-07-24  |  3.0 KB
  1. Path: sparky!uunet!mcsun!uknet!edcastle!dcs.ed.ac.uk!pkdf
  2. From: pkdf@dcs.ed.ac.uk (Peter Froome)
  3. Newsgroups: comp.software-eng
  4. Subject: SpecBox: a formal methods tool for VDM
  5. Message-ID: <39834@skye.dcs.ed.ac.uk>
  6. Date: 24 Jul 92 15:21:52 GMT
  7. Sender: nnews@dcs.ed.ac.uk
  8. Reply-To: pkdf@dcs.ed.ac.uk (Peter Froome)
  9. Organization: Laboratory for the Foundations of Computer Science, Edinburgh U
  10. Lines: 74
  11.  
  12. SPECBOX VERSION 2.21
  13. ____________________
  14.  
  15. A new version of Adelard's formal specification support tool for 
  16. draft BSI/ISO VDM has now been released.  The new version has several 
  17. improvements and enhancements over older versions, including the 
  18. following:
  19.  
  20. *    A revised grammar, reflecting the latest draft standard
  21. *    An improved LaTeX facility
  22. *    An improved, much faster, semantic analyser
  23. *    An interface to the Mural proof assistant
  24.  
  25. Prices now run from 495 to 1995 UK pounds for single user supported 
  26. licences, with academic site licences between 250 and 500 UK pounds.
  27.  
  28.  
  29. DESCRIPTION
  30.  
  31. SpecBox is an industrialised tool for inputting, checking and 
  32. printing VDM specifications.  It is composed of four main parts:
  33.  
  34. *    A syntax checker
  35. *    A LaTeX generator
  36. *    A semantic analyser
  37. *    A Mural translator
  38.  
  39. The syntax checker is used to input specifications in the ASCII form 
  40. of BSI/ISO VDM and check them for grammatical errors.  The checker 
  41. comprises an editor linked to a parser; it gives help on the valid 
  42. VDM terms to enter at each stage, and also enables the grammar to be 
  43. investigated and particular syntactic classes to be chosen.  It also 
  44. completes phrases (by closing brackets, for example) automatically.
  45.  
  46. The LaTeX generator produces a source file for the LaTeX document 
  47. preparation system that will print the specification in the 
  48. mathematical syntax.  Line numbering, cross-references and subscripts 
  49. are supported.
  50.  
  51. The semantic analyser carries out checks on the well-formedness of 
  52. the specification.  These checks include matters such as declaration, 
  53. scope, number of arguments, use of state variables and hooked values, 
  54. use of record types and constructor functions, and use of 'is-
  55. expressions'.  The semantic analyser displays diagnostic messages 
  56. while it is running, and on completion produces a report file, an 
  57. annotated listing and a cross-reference table.  The algorithm used 
  58. for analysis prevents many redundant cascade error messages from 
  59. being generated after the first occurrence of a semantic problem.
  60.  
  61. The Mural interface enables specifications produced using SpecBox to 
  62. be transmitted to the Mural proof assistant for the generation and 
  63. discharge of proof obligations.  (Mural was developed by Manchester 
  64. University and the Rutherford Appleton Laboratory.)
  65.  
  66. SpecBox is continually being enhanced: future developments include
  67.  
  68. *    A version for Microsoft Windows 3.1
  69. *    Mathematical syntax support
  70. *    Full support for BSI/ISO VDM modules
  71.  
  72. Existing customers receive upgrades at preferential prices.
  73.  
  74.  
  75. For further information contact:
  76.  
  77. Peter Froome
  78. Adelard
  79. Coborn House
  80. 3 Coborn Road
  81. London E3 2DA
  82. UK
  83. Tel: +44 (0)81 983 0214
  84. Fax: +44 (0)81 983 1845
  85. Email: pkdf@dcs.ed.ac.uk
  86.