码迷,mamicode.com
首页 > 其他好文 > 详细

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

时间:2014-11-12 22:56:40      阅读:303      评论:0      收藏:0      [点我收藏+]

标签:style   blog   http   io   color   ar   os   使用   java   

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

bubuko.com,布布扣

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

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

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

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

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

bubuko.com,布布扣

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

bubuko.com,布布扣

 

2.Now Let us Start!


理论说明了一大堆,现在终于可以开始实战了!如何实现从用户需求到VDM++的转化呢!? 

2.1 用户需求

bubuko.com,布布扣

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

bubuko.com,布布扣

(2)输入Project Name

bubuko.com,布布扣

(3)选择导入IO Library

bubuko.com,布布扣

2.3.2 新建Library文件

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

bubuko.com,布布扣

2.3.3 定义必要的类和数据类型(代码后附)

bubuko.com,布布扣

2.3.4 定义操作operations

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

bubuko.com,布布扣

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

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

bubuko.com,布布扣

2.3.6 补全操作体

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

bubuko.com,布布扣

2.3.7 补全instance variables

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

bubuko.com,布布扣

2.3.8 根据需求定义函数functions

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

bubuko.com,布布扣

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->如图:

bubuko.com,布布扣

(2)点击运行,弹出如下窗口:

bubuko.com,布布扣

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

bubuko.com,布布扣

结果显示为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);
    }
}

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

标签:style   blog   http   io   color   ar   os   使用   java   

原文地址:http://www.cnblogs.com/Kassadin/p/4093664.html

(0)
(0)
   
举报
评论 一句话评论(0
登录后才能评论!
© 2014 mamicode.com 版权所有  联系我们:gaon5@hotmail.com
迷上了代码!