接前文：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++的图书管理系统需求定义