首页 > 代码库 > 【形式化方法：VDM++系列】4.VDM实战1——铁路费用计算
【形式化方法：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.
使用函数计算两个车站之前的铁路费用。基础数据如下：
valuesvFareSet = {mk_FareRecord("Tokyo", "Shinagawa", 220),mk_FareRecord("Tokyo", "Shinjuku", 180),mk_FareRecord("Shinjuku", "Shinagawa", 190)}
函数开头如下：
static public Calculate_fare : set of FareRecord * Station * Station -> natCalculate_fare(aSetOfFare, aDeparture, anArrival) == is not yet specified;
2.解法
首先必须明确问题要求，仔细观察函数的输入输出，Calculate_fare函数有3个输入参数，分别是费用记录集合（set of FareRecord），始发车站，终点车站；输出为一个整数，即2个车站间的费用；函数内容尚未定义，现在需要我们定义函数体完成费用的计算。
计算费用的业务逻辑是：根据始发站和终点站查找费用记录集合，如果在费用纪录集合中找到始发站和终点站都相同的纪录，就返回该记录的费用。用SQL语言可以很简单的解释该逻辑：
select fare_num from fareRecord where fareRecord.aDeparture=aDeparture and fareRecord.anArrival=anArrival
明确了业务逻辑就可以打开Overture工具开始码了！
上图展示了Overture工具默认建立的vdm类，它包类定义，类型定义，值定义，初始化变量，操作定义，函数定义，测试用例定义。这里我们需要定义type，value和functions
（1）定义类型
需要定义的类型有：fareRecord类型，Station类型。
定义Station类型与String等价，定义FareRecord类型为结构体类型，包含3个子元素
（2）定义值
（3）定义函数
注意：红线部分所展示的函数体与之前的SQL语句基本相同，let .. in set .. be st .. in .. 是VDM＋＋独特的语法所在，需要仔细体会才能明白。
（4）定义函数的前置条件和后置条件
函数的前置条件是：对于要求的始发站和终点站应该包含于费用记录集合当中，对于费用记录集合中的2条记录，如果始发站和终点站相同，那么费用也应该相同。
函数的后置条件是：存在唯一一条记录，该记录的始发站，终点站与传入的始发站，终点站相同，该记录的结果与执行函数体得到的result相同。
至此，我们的需求定义完成。
代码如下：
class fareCaculatetypespublic Station = seq of charinv s == s<>"";public FareRecord :: fDeparture : Station fArrival : Station fFare : natinv fr == fr.fDeparture <> fr.fArrivalfunctionsstatic public Calculate_fare : set of FareRecord * Station * Station -> natCalculate_fare(aSetOfFare, aDeparture, anArrival) ==let wFareRecord in set aSetOfFare be st{aDeparture, anArrival} = {wFareRecord.fDeparture, wFareRecord.fArrival}in wFareRecord.fFarepre{aDeparture, anArrival} in set{{e.fDeparture, e.fArrival} | e in set aSetOfFare} andforall wFareRecord1, wFareRecord2 in set aSetOfFare &wFareRecord1.fDeparture = wFareRecord2.fDeparture andwFareRecord1.fArrival = wFareRecord2.fArrival =>wFareRecord1.fFare = wFareRecord2.fFarepostexists1 wFareRecord in set aSetOfFare &{aDeparture, anArrival} = {wFareRecord.fDeparture, wFareRecord.fArrival} andRESULT = wFareRecord.fFare;end fareCaculate
3.测试
现在编写测试程序对上述需求进行测试。测试程序如下所示：
class Test is subclass of fareCaculatevalues vFareSet = { mk_FareRecord("Tokyo","Shinagawa",220), mk_FareRecord("Tokyo","Shinjuku",180), mk_FareRecord("Shinjuku","Shinagawa",190)};functionsstatic public makeOrderMap : seq of bool +> map nat to boolmakeOrderMap(s) == {i |-> s(i) | i in set inds s};public run : () -> seq of char * bool * map nat to boolrun() ==let testcases = [t1(), t2(), t3()],testResults = makeOrderMap(testcases)inmk_("The result of regression test = ",forall i in set inds testcases & testcases(i), testResults);public t1 : () -> boolt1() ==Calculate_fare(vFareSet, "Tokyo", "Shinagawa") = 220;public t2 : () -> boolt2() ==Calculate_fare(vFareSet, "Tokyo", "Shinjuku") = 180;public t3 : () -> boolt3() ==Calculate_fare(vFareSet, "Shinjuku", "Shinagawa") = 190;end Test
测试结果如图所示：
测试全部返回true，表明需求定义正确。
至此，第一版的的铁路票价计算需求定义程序完成。
【形式化方法：VDM++系列】4.VDM实战1——铁路费用计算