又有將近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 : StationfArrival : StationfFare : nat inv fr == fr.fDeparture <> fr.fArrivalfunctions 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 fareCaculatevalues 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，表明需求定義正確。

至此，第一版的的鐵路票價計算需求定義程序完成。

?

轉載于:https://www.cnblogs.com/Kassadin/p/4213683.html

總結

以上是生活随笔為你收集整理的【形式化方法：VDM++系列】4.VDM实战1——铁路费用计算的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。