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

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

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 定义必要的类和数据类型（代码后附）

2.3.4 定义操作operations

需要注意的是，由于VDM的主要作用在于需求描述，因此在VDM++中操作体不是最重要的要素，可以先不定义，在这里，我就用了is not yet specified把操作体先留空。

2.3.5 定义操作的前置条件和后置条件

pre-condition和post-condition是大部分形式化方法最重要的特点！！他们定义了操作的前提和结果，通常我们会使用post条件进行结果检查与测试，他们的作用通常比操作体本身还要重要。

2.3.6 补全操作体

add_user方法操作体只有1行，即求sUsers和aUser的并集，合并后赋值给sUsers

2.3.7 补全instance variables

补充sBorrowing映射实例的定义域和值域（这对于map类型非常重要），其定义域为sCopies的子集，其值域为sUsers的子集；即把书借给用户

2.3.8 根据需求定义函数functions

这里由于多处用到了判断某本书是否被借走，为了避免重复，我们应该定义一个函数封装该功能。

2.3.9 代码编写完成，全部代码如下：

class Library
--类型定义
types
public Copy = token ;
public User = token ;
Borrowing = map Copy to User;

--实例定义和初始化
instance variables
sCopies : set of Copy := {};
sUsers: set of User := {};
sBorrowing: Borrowing := { |-> };
--定义map类型实例的定义域和值域
inv
    dom sBorrowing subset sCopies and
    rng sBorrowing subset sUsers;

operations
--定义操作，操作名add_user,输入参数类型User，返回值为空
public add_user : User ==> ()
--定义操作体，此处还尚未定义
add_user(aUser) ==
sUsers := sUsers union {aUser}
--定义操作的前置条件和后置条件
--前置条件：aUser不在sUsers中
--后置条件：aUser加入了sUsers集合
pre
    aUser not in set sUsers
post
    sUsers = sUsers~ union {aUser};

public remove_user : User ==> ()
remove_user(aUser) ==
    sUsers := sUsers \ {aUser}
pre
    aUser in set sUsers and
    not borrowedUser(sBorrowing, aUser)
post
    sUsers = sUsers~ \ {aUser};

public add_book : Copy ==> ()
add_book(aCopy) ==
    sCopies := sCopies union {aCopy}
pre
    aCopy not in set sCopies
post
    sCopies = sCopies~ union {aCopy};

public remove_book: Copy ==> ()
remove_book(aCopy) ==
    sCopies := sCopies \ {aCopy}
pre
    aCopy in set sCopies and
    not borrowedCopy(sBorrowing, aCopy)
post
    sCopies = sCopies~ \ {aCopy};

public borrow_book : User * Copy ==> ()
borrow_book(aUser, aCopy) ==
    sBorrowing := sBorrowing munion {aCopy |-> aUser}
pre
    aUser in set sUsers and
    aCopy in set sCopies and
    not borrowedCopy(sBorrowing, aCopy)
post
    sBorrowing = sBorrowing~ munion {aCopy |-> aUser};

public return_book : Copy ==> ()
return_book(aCopy) ==
    sBorrowing := {aCopy }<-: sBorrowing
pre
    borrowedCopy(sBorrowing, aCopy)
post
    sBorrowing = {aCopy } <-: sBorrowing~;

public getAttributes : () ==> set of Copy * set of User * map Copy to User
getAttributes() == return mk_(sCopies, sUsers, sBorrowing);

functions
--函数定义，该函数判断该书是否已经被借走，输入参数是Borrowing类型和Copy类型，如果被借走则返回true
borrowedCopy : Borrowing * Copy +> bool
borrowedCopy(aBorrowing, aCopy) ==
    aCopy in set dom aBorrowing;

borrowedUser : Borrowing * User +> bool
borrowedUser(aBorrowing, aUser) ==
    aUser in set rng aBorrowing;

end Library

需要注意的是，现在没有必要纠缠于语法细节，对于每一部分的具体语法，会在后续文章陆续介绍。本次的关注点主要在于概览VDM++的开发过程，程序基本结构，基本概念等要素，而不是具体的语法细节。

2.4 编写测试类

程序编写完了，总需要看看运行结果吧；很显然现在这个程序没有运行结果，原因很简单，只有类定义，没有相应的测试数据。就好比Java程序，定义了一个类，但是没有写main函数一样，因此，我们必须编写测试类，测试所写的Library需求。

这里，我直接提供一个简单的测试类。

class UseLibrary

instance variables
sL : Library :=  new Library();

functions
public run : () -> seq of char * bool * map nat1 to bool
run() ==
    let testcases = [
            t1()
        ],
        testResults = makeOrderMap(testcases)
    in
    mk_("The result of regression test = ", forall i in set inds testcases & testcases(i), testResults);

static public makeOrderMap : seq of bool +> map nat1 to bool
makeOrderMap(s) == {i |-> s(i) | i in set inds s}
pre s <> [];

operations
t1: () ==> bool
t1() ==
    let l = new Library(),
        p = mk_token("Sakoh"),
        c = mk_token("OO Construction_1")
    in (
        l.add_user(p); l.add_book(c); l.borrow_book(p, c); l.return_book(c); l.remove_user(p);
        return
            l.getAttributes() = mk_({mk_token("OO Construction_1")}, {}, {|->})
    );
end UseLibrary

该测试类添加了一个实例，l是一个Library实例，p是一个User实例，c是一个Copy实例，我们对l进行添加用户，添加图书，借书，还书，删除用户等一系列操作，最后比较l中的所有属性值与给定属性值mk_({mk_token("OO Construction_1")}, {}, {|->})是否相等，即判断是否符合预期。如果返回true，则该测试用例通过，需求定义合理；否则，该测试用例不通过，需求定义不符合要求。

2.5 测试结果

（1）修改run configuration

右键工程，Run As->run configurations->如图：

（2）点击运行，弹出如下窗口：

（3）输入print new UseLibrary().run()查看运行结果是否符合预期

结果显示为true，说明测试用例通过。

3.After Coding


至此，我们的图书管理系统需求定义基本完成（其实还有很多没有做，如测试覆盖率检查，需求文档生成等等）。VDM++已经向我们展示了它的强大功能。在后续部分，我会逐步解释VDM++的语法特征和具体用法，敬请期待。

最后来看看我们的VDM代码被转化成了哪些Java代码吧！

右键工程，Code Generation->Generate Java

import org.overture.codegen.runtime.*;

import java.util.*;

public class Library {
    private VDMSet sCopies = SetUtil.set();
    private VDMSet sUsers = SetUtil.set();
    private VDMMap sBorrowing = MapUtil.map();

    public Library() {
    }

    public void add_user(final Token aUser) {
        sUsers = SetUtil.union(sUsers.clone(), SetUtil.set(aUser));
    }

    public void remove_user(final Token aUser) {
        sUsers = SetUtil.diff(sUsers.clone(), SetUtil.set(aUser));
    }

    public void add_book(final Token aCopy) {
        sCopies = SetUtil.union(sCopies.clone(), SetUtil.set(aCopy));
    }

    public void remove_book(final Token aCopy) {
        sCopies = SetUtil.diff(sCopies.clone(), SetUtil.set(aCopy));
    }

    public void borrow_book(final Token aUser, final Token aCopy) {
        sBorrowing = MapUtil.munion(sBorrowing.clone(),
                MapUtil.map(new Maplet(aCopy, aUser)));
    }

    public void return_book(final Token aCopy) {
        sBorrowing = MapUtil.domResBy(SetUtil.set(aCopy), sBorrowing.clone());
    }

    public Tuple getAttributes() {
        return Tuple.mk_(sCopies.clone(), sUsers.clone(), sBorrowing.clone());
    }

    private static Boolean borrowedCopy(final VDMMap aBorrowing,
        final Token aCopy) {
        return MapUtil.dom(aBorrowing.clone()).contains(aCopy);
    }

    private static Boolean borrowedUser(final VDMMap aBorrowing,
        final Token aUser) {
        return MapUtil.rng(aBorrowing.clone()).contains(aUser);
    }
}
时间： 2024-10-09 21:41:42

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

【形式化方法：VDM++系列】4.VDM实战1——铁路费用计算

又有将近2个月没更新博客了啊!winter holiday简直玩儿疯了的说!结果假期前学习的形式化方法已经忘了大半!面对期末作业,大脑一片空白.于是,赶快复习了一下之前学习的姿势! 这次的主要任务是完成一个费用计算程序. 1.问题 Make a model to calculate train fare from a station to another station by using functions and the following table. 使用函数计算两个车站之前的铁路费用.基

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

接前文: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/ [O

【形式化方法：VDM++系列】1.前言

1.前言 今天开始上课学习软件需求分析与VDM++,经过一节课的学习,我又增长了见识. 软件需求工程在软件工程中处于十分核心的地位:需求分析的好坏直接决定软件工程的成败.这一点是我之前对需求工程的理解和认识,然而今天的学习又进一步扩展了我的认识. 2.需求分析的发展阶段 说起需求分析,首先想到的是用例,然后就是各种各样的用例图,功能描述:接下来我会想到产品原型,业务流程描述等等:然而这些其实都只是需求工程的某一阶段的一小部分.实际上,需求分析大致可划分为以下3个阶段: (1)上世纪70年代兴起的

基于flask的图书管理系统-蓝图

基于flask的图书管理-- 蓝图方式 效果图, 只有基本的增删功能 目录 app 应用名 templates 存放模板, html之类的 book 用于区分html文件 index.html 主页展示 view 存放视图 __init__ 初始化蓝图 bookManage.py 视图函数 __init__ 这个是app的类 , 初始化文件 model.py 数据库模型 manage.py 启动 migrations 这个是flask-migrate生成的, 用于迁移数据库 requiremen

《软件工程 ——理论、方法与实践》知识概括第五章 软件工程中的形式化方法

第5章 软件工程中的形式化方法    从广义上讲,形式化方法(Formal Method)是指将离散数学的方法用于解决软件工程领域的问题,主要包括建立精确的数学模型以及对模型的分析活动.狭义的讲,形式化方法是运用形式化语言,进行形式化的规格描述.模型推理和验证的方法.将形式化方法运用于软件工程实践当中的只要目的是保证软件的正确性. 软件生命周期中的形式化转化策略:常用转化策略.直接转化策略和运用半形式化表示的中间转化策略. 进行模型化的过程中涉及到三种系统模型:现实世界.模型表示和计算机系统.

基于DDD的现代ASP.NET开发框架--ABP系列之7、ABP Session管理

点这里进入ABP系列文章总目录 基于DDD的现代ASP.NET开发框架--ABP系列之7.ABP Session管理 ABP是“ASP.NET Boilerplate Project (ASP.NET样板项目)”的简称. ABP的官方网站:http://www.aspnetboilerplate.com ABP在Github上的开源项目:https://github.com/aspnetboilerplate 简介 如果一个应用程序需要登录,则它必须知道当前用户执行了什么操作.因此ASP.NET

软件工程——理论、方法与实践 之 软件工程中的形式化方法

软件工程——理论.方法与实践 之 软件工程中的形式化方法 从广义上讲,形式化方法是指将离散数学的方法用于解决软件工程领域的问题,主要包括建立精确的数学模型以及对模型的分析活动.狭义的讲,形式化方法是运用形式化语言,进行形式化的规格描述.模型推理和验证的方法.形式化方法运用于软件工程实践当中主要目的是保证软件的正确性.软件开发实际上就是把现实世界的需求映射成软件额模型化过程.该过程包括:形式规约.形式证明我与检验.程序求精三方面的活动. 形式化规格说明是对软件系统对象,对象的操作方法,以及对象行为

软件工程中的形式化方法

软件的设计过程就是一个建立形式规约的过程.软件开发实际上就是把现实世界的需求映射成软件的模型化方法.软件规格说明是对软件系统对象,对象的操作方法,以及对象行为的描述.形式证明与验证技术主要包括模型检测和定理证明.程序求精是将自动推理和形式化方法相结合,从抽象的形式规约推演出具体的面向计算机的程序代码的全过程.模态(Modal)逻辑是经典命题逻辑和一阶谓词逻辑的扩展形式.Kripke结构.1.一阶线性时态逻辑(FOLTL)是一阶谓词逻辑的扩展.2.计算树逻辑(CTL)是一种离散.分支时间.命题时态

软件工程概论第五章--软件工程中的形式化方法

形式化方法指的是将离散数学的方法用于解决软件工程领域的问题,主要是建立精确的数学模型以及对模型的分析活动.在软件开发过程中运用数学模型有很多优点,例如能够解决规格说明的二义性,提高精确性,还能使软件相关问题的本质可以在不同抽象层次被展示出来.本章介绍形式化方法主要从形式化方法基本概念.时态逻辑.模型检验.Z语言.Petri网几个方面讲述. 形式化方法基本概念主要讲了形式规范.形式证明与验证.程序求精,形式规范说明是对软件系统对象,对象的操作方法,以及对象行为的描述.形式证明与验证主要包括模型检测