|
| |
VDM-Tools
|
IFAD
offers tools that allows one to develop and analyze precise
models of computing systems, based on an internationally standardized notation.
When used in the early stages of system development, such a model can serve
as a system specification, as an aid in checking the consistency and
completness of user requirements, as a blueprint for system design and/or coding.
Currently, IFAD offers the two following tools:
About VDM-SL
A model in VDM-SL contains definitions of data and functionality of a system.
Besides simple basic types such as characters and numbers, VDM-SL also
supports high level types such as sets, sequences and maps. Values of
these basic types can be grouped into more elaborate types such as records
sets, sequences and mappings. Types may be restricted by invariants.
The notation allows one to choose a level of abstraction appropriate for
the analysis at hand.
In contrast, a model in a traditional programming language may have
to contain machine-specific details not relevant to the problem.
Funtionality in a VDM-SL is defined through function and operation
definitions. For each function, the types of the input and result
are given. The input values to which a function may be applied can
be restricted by means of the pre-condition. An indirect (implicit)
function definition uses postcondition that states only the properties
of the result without employing any particular algorithm.
In contrast, an explicit (direct) function definition does provide an "algorithm"
in the form of an expression returned. If a real algorithm is needed,
however, one needs to use operations rather than functions.
IFAD's Toolbox provides a syntax and type checking mechanism and, for
a direct specification, the Toolbox can interpret it.
Moreover,
- C++ code can be generated for a direct specification;
- The user can link an existing C++ library function to the
VDM-SL model under development
About VDM++
VDM++ provides an object-oriented version of the standard notation. Besides
supporting most of the standard, the VDM++ Toolbox provides a Corba compliant Application
Programmer Interface (API), which allows other programs to access a running Toolbox.
Thus, any code such as a graphical front-end or existing legacy code may
control any Toolbox component.
Also, there is a Rose-VDM++ Link that integrates UML and VDM++. It provides
a bi-directional translation which gives a tight coupling between the Toolbox and
Rational Rose.
Please visit http://www.ifad.dk to learn more about VDM-SL.
Currently, the VDM-SL Toolbox is used in two courses:
- CSE 437/537, Systematic Software Development,
where it supports a nontrivial term project.
- CSE 510, Fundamentals of Software Engineering Modelling,
where only the “expression” part of the notation is used to
help students check their mathematical skills.
To learn more about VDM-SL/VDM++ and their use in industry and academia
visit the following sites:
For Instructions on How to Use -VDM-SL- Click Here.
|
