1.Before We Start：

在开始图书管理系统需求定义之前，需要先进行一些说明。

1.1 输入，输出定义

输入：用户需求文字说明

输出：基于VDM++的需求规格说明文档

任何问题只有明确它的输入和输出，才会有一个明确的预期，才有可能获得预期的结果。在这里明确问题的输入输出更加重要。特别需要指出的是，VDM++作为一种形式化方法语言，它主要用于需求分析，而不是代码实现。虽然它的产出是一段一段的代码，但如果你期望通过VDM++得到现成的系统实现代码，很抱歉，我们无法得到预期的输出。

VDM++不是Java这类系统实现的语言，它的输出结果不是Web网站，不是GUI程序，甚至连命令行程序都实现不了。想到这些，难免有些失落，总觉得失去了编程的那种成就感；但这就是事实，这或许也是形式化方法难于普及的原因之一。

1.2 VDM的理论探讨

那么，VDM++的输出是什么呢？如前文所述，其输出是需求规格说明书（需求文档），编写需求文档可以采用以下几种描述方法：

a.自然语言描述（最通俗易懂的方法，但不标准，歧义较多）

b.结构化系统分析方法——流程图，数据流图，数据字典等（上世纪70年代结构化思想的产物，与自然语言相比更加规范，更加接近计算机语言）

c.OOD方法——UML建模（上世纪80年代面向对象思想的产物，时至今日仍然有很大的影响力，特点是半结构化，需求描述规范清晰，可通过一定的框架转化为实际代码，仍然是主流的系统分析与设计技术）

d.形式化方法——VDM,Z方法等(上世纪90年代开始逐渐发展起来的软件工程方法，采用类似于编程语言的代码形式描述软件需求，特点是完全结构化，形式化，自动化)

由此可见，如果要在软件工程中找到一个可以和VDM类比的东西的话，我个人认为应该是UML；或许我们应该把VDM++的代码理解为各种各样的用例图，活动图，类图。形式化方法的主要作用领域是在软件开发中的上游工程（即需求，设计，自动化测试等），而不是具体的编码实现。

这些许令人有些失望，辛辛苦苦写出来那么多的VDM代码，居然不能作为系统实现的代码；那我为什么还要写这些东西呢？

1.3 VDM++的作用范围

这里，我详细阐述一下VDM++能做些什么！？具体请参考该网站：http://monoist.atmarkit.co.jp/mn/articles/0810/20/news106.html

1.编写需求规格说明书，检查需求分析结果和用户需求的一致性

2.检查需求规格说明书，系统设计文档的正确性

3.检查需求规格说明书，系统设计文档的一致性

4.为下游工程提供自动化测试用例

通过形式化方法，最终的理想目标是实现软件工程化，自动化，精确化，标准化；实际结果是减少需求工程中的不一致性（如下图），降低软件开发的时间（人月），提高软件开发效率，保证系统开发结果与客户需求相一致。

上图形象地阐释了客户需求和软件最终产品的鸿沟，已成为软件工程经典案例，这里不再赘述。下图解释了形式化方法与软件工程的关系：

2.Now Let us Start！

理论说明了一大推，现在终于可以开始实战了！如何实现从用户需求到VDM++的转化呢！？

2.1 用户需求

1.开发一个计算机系统用于管理图书的借还

2.实现用户管理

3.实现图书管理

4.用户可以进行图书借还

为了简化问题，这里的需求非常的简单——只有4句话，现在我们要做的就是细化这些需求。

2.2 需求的细化

（1）首先我们明确我们需要开发一个图书管理系统（Library System）

（2）其次，我们抽取出系统实体和系统参与者的活动（和用例图建模一样）

系统实体：Library，User，Book

活动：borrow books，return books，manage users，manage books

（3）抽取相应的操作

borrow_book,return_book,add_user,remove_user,add_book,remove_book

2.3 开始编码

【VDM++的语法还是比较多的，这里我们不能纠缠于VDM的语法细节，这些语法细节会在之后慢慢解释】

2.3.1 建立项目

（1）打开Overture Tool，新建Project

（2）输入Project Name

(3)选择导入IO Library

2.3.2 新建Library文件

在项目上点击右键，New->Empty VDMPP File,输入文件名

2.3.3 定义必要的类和数据类型（代码后附）

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