OO第三次博客總結

時間 2019-12-08

標籤第三次博客總結简体版

原文原文鏈接

1、規格發展歷史

從20世紀60年代開始，就存在着許多不一樣的形式規格說明語言和軟件開發方法。在形式規格說明領域一些最主要的發展過程列舉以下：git

1969－1972 C.A.R Hoare撰寫了"計算機編程的公理基礎（An Axiomatic Basis for Computer Programming）"和"數據表示的正確性證實"兩篇開創性的論文，並提出了規格說明的概念。編程

1974－1975 B.Liskow/S.N. Zilles和J. Guttag引入了"抽象數據類型"的概念。測試

1976 E.W. Dijkstra定義了"最弱前置條件"的概念this

1977 R.Burstall和J.Goguen提出了第一個代數規格說明語言：Clearspa

1988 Standford的SRI開發了代數規格說明語言OBJ3對象

1980-1986 C.Jones定義了VDM語言，也就是維也納開發方法。ci

1985－1992 牛津大學的程序研究小組開發了Z規格說明語言。與此同時BP研究室開發了稱之爲B方法的面向模型的規格說明語言。element

1985－1993 在MIT和Digital SRC開發了代數規格說明語言Larch開發

從1991年開始，面向對象的形式規格說明語言開始發展，例如，Object-Z, VDM++, CafeOBJ等語言。it

1996－2000年在歐洲CoFI（Common Framework Initiative）項目資助下開發"統一"代數規格說明語言CASL(Common Algebraic Specification Language)

上述規格說明語言能夠分爲兩大類：

l 基於代數和公理方法（Clear, OBJ, Larch, CafeOBJ）

l 基於模型的方法（VDM, Z, B, Object-Z）

2、 bug統計及分析

	功能bug	規格bug	是否有聯繫
第9次做業	2	1	無
第10次做業	5	0	是
第11次做業	3	0	是

分析：

規格化的BUG由於當時助教羣裏沒有要求必須使用布爾表達式，因此當時使用了大量的天然語言，結果就被同窗上報了一個complete這個之後會格外注意，不會在使用天然語言。至於功能上的BUG，有的能被同窗測試出來我比較感激，有的就不能使我信服，在持續申訴中，同窗指出的讓我比較感激的BUG有關於信譽度的選擇，應該選擇信譽度最高的出租車，由於當時閱讀指導書不夠仔細，因此優先選擇了距離比較近的其次是信譽度最高的，已作改正，還有是關於流量問題的，由於指導書變動了爲道路總流量，而我只在每一步行走的時候選擇了一個流量最小的道路，因此被報了一個BUG。讓我比較迷的BUG在於被亂報關於紅綠燈的問題，一會兒報了好幾個，就粘貼一段個人代碼，說我寫的有問題我以爲非常不能接受。但願這種現象會愈來愈少。

3、規格舉例

　　１、能夠用布爾表達式可是使用了天然語言　

　　　 /**@REQUIRES:
　　　 *@MODIFIES: this
　　　　*@EFFECTS: 若是taxi沒有初始化就給taxi賦值
　　　　*@THREAD_REQUIRES:
　　　　*@THREAD_EFFECTS:
　　　　*/

　　　改進後：

　　　/**@REQUIRES:
　　　 *@MODIFIES: this
　　　　*@EFFECTS: (init==true)==>(a=new taxi())
　　　　*@THREAD_REQUIRES:
　　　　*@THREAD_EFFECTS:
　　　　*/

　　二、沒有關於異常的信息

　　　　/** @REQUIRES:
　　　 *@MODIFIES:
　　　　*@EFFECTS:(a.contains(b))== > \result ==b;

　　　　*@THREAD_REQUIRES:
　　　　*@THREAD_EFFECTS:
　　　　*/

　　改進後

　　　　/**@REQUIRES:
　　　 *@MODIFIES:
　　　　*@EFFECTS: (a.contains(b))== > \result ==b;

　　　　 otherwise==>NoSuchelement

　　　　*@THREAD_REQUIRES:
　　　　*@THREAD_EFFECTS:
　　　　*/

　　三、直接在effect裏粘貼代碼

　　/**@REQUIRES:
　　　 *@MODIFIES:
　　　　*@EFFECTS:(taxi!=null && requelist!=null)

　　　　*@THREAD_REQUIRES:
　　　　*@THREAD_EFFECTS:
　　　　*/

　　改進後:

　　/**@REQUIRES:
　　　 *@MODIFIES:
　　　　*@EFFECTS:(taxi!=null && requelist!=null)==>\result=true

　　　　　　　　　　 otherwise==>\result=false;

　　　　*@THREAD_REQUIRES:
　　　　*@THREAD_EFFECTS:
　　　　*/

　　四、前置條件、後置條件不許確。

　　　　/** @ REQUIRES: r!=null
　　　　@ MODIFIES: this
　　　　@ EFFECTS: RL[len++]=r
　　　　@ THREAD_REQUIRES:
　　　　@ THREAD_EFFECTS:
　　　　@ */

　　　　改進後:

　　　　/** @ REQUIRES: r!=null
　　　　@ MODIFIES: this
　　　　@ EFFECTS: r.repOK()==true ==> (RL[len++]==r) && (RL.contain(r)==true);
　　　　@ THREAD_REQUIRES:
　　　　@ THREAD_EFFECTS:
　　　　@ */