接前文：http://www.cnblogs.com/Kassadin/p/3975853.html

上次讲了软件需求分析的演化过程，本次进入正题——VDM开发环境的搭建

(自从发现能打游戏以来，居然有将近1个月没有写博客了！真是越来越颓废了。。)

其实VDM++已经学习了很多，近几天应该会逐渐更新。

1.VDM开发环境介绍

需要使用的环境主要有2个：（1）VDMTools （2）Overture Tool

官方网站：【VDMTools】http://www.vdmtools.jp/en/

【Overture】http://overturetool.org/languages/

2.安装VDMTools

（1）下载VDMTools首先需要注册账号

（2）账号注册完成后会出现download按钮，点击可以下载

（3）下载完成后，点击安装，一直下一步即可。

（4）安装完成后，如下图所示：

VDMTools的主要功能是对VDM代码进行验证和测试，不能用于编写代码

3.安装Overture Tool

（1）由于Overture Tool是基于Eclipse的，所以运行Overture必须先安装JRE【否则无法运行Eclipse，安装过程略】

（2）在Overture官网下载压缩包

（3）解压，运行Overture.exe即可（其它平台类似）

（4）运行效果如下图：

Overture Tool是VDM++的一个集成开发环境，支持代码编写，代码测试，回归测试，测试分析等一系列功能。主要用于代码编写！

至此，VDM开发环境搭建完成。

4.VDMTools第一步：Hello World程序

安装完了开发环境，想必大家都已经跃跃欲试了，这个VDMTools究竟怎么用呢！？本部分讲解如何使用VDMTools运行第一个程序。

（1）进入VDMTools，点击Interpreter按钮，或者从windows菜单中选择interpreter，进入VDM++解释器。这是VDM++语言的交互式运行环境，类似于python的交互模式，ruby的irb；在该解释器中输入VDM++命令，即可交互式的显示出命令的执行结果，非常适合学习。

（2）如下图，在交互式窗口中输入：p “Hello,world”,点击回车，交互式窗口成功打印出Hello World。至此，HelloWorld程序便开发完成了！怎么样，是不是很简单呢！

至此，VDM++开发环境已经基本入门，或许现在你仍然十分不解：这个VDM++到底可以做些什么！？这个VDM++语言到底又是什么呢！？

VDM++作为一个软件形式化语言，在软件需求分析和软件测试上有着十分强大的功能。在下一篇文章中，我将通过一个实例会为大家展示VDM++的强大功能，敬请期待。

Next：【形式化方法：VDM++系列】3.基于VDM++的图书管理系统需求定义

【形式化方法：VDM++系列】2.VDMTools环境的搭建