标签:style blog http io ar java sp for 文件
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++的图书管理系统需求定义
标签:style blog http io ar java sp for 文件
原文地址:http://www.cnblogs.com/Kassadin/p/4093016.html