又有将近2个月没更新博客了啊！winter holiday简直玩儿疯了的说！结果假期前学习的形式化方法已经忘了大半！面对期末作业，大脑一片空白。于是，赶快复习了一下之前学习的姿势！
这次的主要任务是完成一个费用计算程序。
1.问题
Make a model to calculate train fare from a station to another station by using functions and the following table.
使用函数计算两个车站之前的铁路费用。基础数据如下：
values vFareSet = { mk_FareRecord("Tokyo", "Shinagawa", 220), mk_FareRecord("Tokyo", "Shinjuku", 180), mk_FareRecord("Shinjuku", "Shinagawa", 190) }
函数开头如下：
static public Calculate_fare : set of FareRecord * Station * Station -> nat Calculate_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 fareCaculate types public Station = seq of char inv s == s<>""; public FareRecord :: fDeparture : Station fArrival : Station fFare : nat inv fr == fr.fDeparture <> fr.fArrival functions static public Calculate_fare : set of FareRecord * Station * Station -> nat Calculate_fare(aSetOfFare, aDeparture, anArrival) == let wFareRecord in set aSetOfFare be st {aDeparture, anArrival} = {wFareRecord.fDeparture, wFareRecord.fArrival} in wFareRecord.fFare pre {aDeparture, anArrival} in set {{e.fDeparture, e.fArrival} | e in set aSetOfFare} and forall wFareRecord1, wFareRecord2 in set aSetOfFare & wFareRecord1.fDeparture = wFareRecord2.fDeparture and wFareRecord1.fArrival = wFareRecord2.fArrival => wFareRecord1.fFare = wFareRecord2.fFare post exists1 wFareRecord in set aSetOfFare & {aDeparture, anArrival} = {wFareRecord.fDeparture, wFareRecord.fArrival} and RESULT = wFareRecord.fFare; end fareCaculate
3.测试
现在编写测试程序对上述需求进行测试。测试程序如下所示：
class Test is subclass of fareCaculate values vFareSet = { mk_FareRecord("Tokyo","Shinagawa",220), mk_FareRecord("Tokyo","Shinjuku",180), mk_FareRecord("Shinjuku","Shinagawa",190) }; functions static public makeOrderMap : seq of bool +> map nat to bool makeOrderMap(s) == {i |-> s(i) | i in set inds s}; public run : () -> seq of char * bool * map nat to bool run() == let testcases = [t1(), t2(), t3()], testResults = makeOrderMap(testcases) in mk_("The result of regression test = ", forall i in set inds testcases & testcases(i), testResults); public t1 : () -> bool t1() == Calculate_fare(vFareSet, "Tokyo", "Shinagawa") = 220; public t2 : () -> bool t2() == Calculate_fare(vFareSet, "Tokyo", "Shinjuku") = 180; public t3 : () -> bool t3() == Calculate_fare(vFareSet, "Shinjuku", "Shinagawa") = 190; end Test
测试结果如图所示：
测试全部返回true，表明需求定义正确。
至此，第一版的的铁路票价计算需求定义程序完成。