comp.software-eng archive file "blurb/IFAD" last changed 9 Jul 1993 IFAD Announces The IFAD VDM-SL Toolbox Version 2.0 The Toolbox is available on the SUN Sparc architecture and supports the development of formal specifications using the latest (December 1992) version of the complete VDM-SL standard. The Toolbox supports extensive semantic checks, latex pretty printing, execution and many debugging facilities. All tools can be elegantly operated through an Emacs interface. VDM-SL ====== One of the most mature formal methods, primarily intended for the formal specification and the subsequent development of functional aspects of software systems, is the Vienna Development Method (VDM). A central element of VDM is its specification language: VDM-SL. VDM-SL is a wide spectrum specification language: it can be used for both highly abstract specifications and for specifications at a very low level of abstraction. The increasing use of VDM, and the growing number of dialects in use has led to the recognition of the need for a VDM standard. The standardization effort is carried out under the auspices of the International Standards Institution (ISO) and the British Standards Institution (BSI). The standard is expected to become an ISO draft for comments standard at a working group meeting in April 1993. TOOLS Syntax Checker ============== The syntax checker supports the full VDM-SL standard. All syntax errors are displayed directly in the source specification through the Emacs interface. Interpreter =========== The interpreter supports execution of most VDM-SL constructs like Higher order functions and Currying, Lambda expressions, Looseness and Exceptions. The only constructs which can not be executed are implicit functions and operations and type-bindings. Given a specification the interpreter supports evaluation of expressions in the environment defined by the specification. One of the benefits of executing specifications is that testing techniques can be used to validate the specifications. In the development process small examples for parts of a specification can be executed to enhance the designer's knowledge of the specification. Furthermore an executable specification can form a running prototype. Pretty Printers =============== The IFAD VDM-SL Toolbox works on the ASCII syntax of VDM-SL. When including VDM specifications in written documentation it is useful to print the specifications in the mathematical syntax. The current pretty printing facility supports the Latex type setting system. It generates Latex macros (the standard NPL VDM-SL macros) which can be included in any latex document. Debugger ======== When working with executable specifications some kind of debugging facility is extremely helpful. A debugger has therefore been developed containing a number of the facilities found in debuggers for ordinary programming languages: - interactively evaluation of expressions - breakpoints - show values of variables - show the call stack with parameter values An emacs lisp interface to the emacs editor is supplied with the debugger, integrating it with emacs in a way very similar to the GNU gdb debugger. Static Semantic Analyzer ======================== An analyzer which supports the static semantics for the full VDM-SL standard has been developed. All detected static semantic errors are displayed directly in the source specification through the Emacs interface. IFAD VDM-SL Toolbox availability ================================ IFAD offers a worldwide release of the IFAD VDM-SL Toolbox. The Toolbox runs on SUN Sparc machines with 8MB of memory and requires 7MB of disk space. The following are the prices and sales conditions for the Toolbox version 2.0 Licenses and prices =================== Standard license costs 25.000 Danish Kroner for the first copy, -15\% for the 2nd and 3rd copy, -30\% for the 4th and 5th copy and -40\% for the following copies. Evaluation license costs 2.000 Danish Kroner. The product can be used for evaluation purposes only. The price covers handling costs only. Educational license costs 3.500 Danish Kroner. This license applies to universities and other educational institutions. The product may not be used in commercial projects under this license. All prices are excl. VAT and all licenses covers use of a copy of the toolbox on one machine/CPU only. Further Information =================== For further information please contact: Poul Boegh Lassen IFAD Forskerparken 10 5230 Odense M Denmark Telephone: +45 65 93 23 00 Fax : +45 65 93 29 99 E-mail: poul@ifad.dk Company Description =================== The Institute of Applied Computer Science is a private high technology institution established in 1986 on request from the industry. It is an economical independent non-profit organization supported by more than 40 companies. The central activity is research and development directed towards areas relevant to industry. A main objective is bridging the gap between the industry and academia. Since its start, IFAD has arranged numerous courses and seminars in the area of design and specification methods, especially methods based on formal specification techniques like VDM. Supported by the Danish government, IFAD has conducted a major survey of existing design and specification methods. IFAD is represented in the BSI Panel which is defining a VDM standard (ISO/ VDM-SL) and is furthermore involved in the standardization of design methods and related areas under the Danish Standards Association and ISO.