OO第三次總結

1、規格化設計的發展歷史

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

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定義了"最弱前置條件"的概念

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

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

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

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

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

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

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

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

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

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

(以上內容來自https://blog.csdn.net/jnucstan/article/details/1724259) 

 

2、bug分析

	功能bug	規格bug	有無聯繫
第9次做業	0	3	無
第10次做業	1	1	無
第11次做業	未測試	未測試	未測試

 

 

 

 

 

 

第9次做業：

本次做業沒有被報功能bug，可是被報了3個JSF的incomplete。第一個是對於已經加鎖的方法，沒有在JSF中說明出對應這一點，THREAD_REQUIRES和THREAD_EFFECTS全爲None；第二個是訪問隊列時的下標i應該知足:\all int i;0<=i可是寫成了None；第三個是大部分JSF使用天然語言書寫。此次做業我剛剛接觸JSF，對於規格化設計的理解還不夠深刻，所以犯了不少錯誤。感謝測試者一一爲我指出，讓我能夠改正。

第10次做業：

本次做業我被報了1個功能bug，其實我以爲這個bug無關緊要，測試者認爲個人sleep(500)有問題，說這樣的話會產生延遲，在sleep時應該用500減去延遲，但是個人輸出所有用的是假時間，延遲多長對輸出並無影響，並且我在寫代碼時已經選擇了避免延遲過大的寫法，可是通過討論以後，我以爲測試者說的也有道理，感受他說的這種sleep方法應該是最合適的寫法，因此最後咱們商議的結果是把error改爲incomplete。本次做業也被報了一個JSF的incomplete：有些簡單邏輯也用了天然語言。其實我在上次做業被報incomplete以後已經把JSF改過一遍，可是惟獨bfs這個類忘記改了，因而就被報了incomplete，這是吃了不仔細的虧。

第11次做業

寫本次做業時，我認真修改了以前關於JSF的全部問題，把天然語言的使用頻率降到最低，並把邏輯表達式檢查了一遍，並且認真添加了新代碼，寫了設計文檔，可是。。。測試者並無給我測試。

 

3、規格bug產生緣由的分析

一開始是看課件和Guideline看的不夠認真，沒有理解其精髓，並且時間緊迫，因而就大面積使用天然語言，並且邏輯寫得不夠仔細。以後對JSF進行了全面修改，可是由於少改了一個類的JSF而又被報了bug。最後一次做業我把JSF所有檢查了一遍，雖然此次做業測試者沒有給我測試，可是我以爲即便他測試了那也很難再挑出JSF的bug了。

 

4、規格的很差寫法與改進

 一、REQUIRES使用天然語言

/**@ REQUIRES:x和y都大於等於0且小於等於79;
 @ MODIFIES:None;
 @ EFFECTS:\result == lightstatus[x][y];
 @ THREAD_REQUIRES:None;
 @ THREAD_EFFECTS:\locked();
 @ */

改正：

/**@ REQUIRES:(x >= 0)&&(x <= 79)&&(y >= 0)&&(y <= 79);
 @ MODIFIES:None;
 @ EFFECTS:\result == lightstatus[x][y];
 @ THREAD_REQUIRES:None;
 @ THREAD_EFFECTS:\locked();
 @ */

二、忽略了必要的REQUIRES

/**@ REQUIRES:None;
 @ MODIFIES:None;
 @ EFFECTS:\result == queue[i].time;
 @ THREAD_REQUIRES:None;
 @ THREAD_EFFECTS:None;
 @ */

改正：

/**@ REQUIRES:(i >= 0)&&(i <= rear);
 @ MODIFIES:None;
 @ EFFECTS:\result == queue[i].time;
 @ THREAD_REQUIRES:None;
 @ THREAD_EFFECTS:None;
 @ */

 

三、EFFECTS使用天然語言

/**@ REQUIRES:(i >= 0)&&(i <= rear);
 @ MODIFIES:None;
 @ EFFECTS:返回queue[i].time;
 @ THREAD_REQUIRES:None;
 @ THREAD_EFFECTS:None;
 @ */

改正：

/**@ REQUIRES:(i >= 0)&&(i <= rear);
 @ MODIFIES:None;
 @ EFFECTS:\result == queue[i].time;
 @ THREAD_REQUIRES:None;
 @ THREAD_EFFECTS:None;
 @ */

四、沒有歸納異常狀況

/**@ REQUIRES:None;
 @ MODIFIES:this;
 @ EFFECTS:(\old(this).get(index) !=null) ==> (this.size == \old(this).size-1) && (this.contains(\old(this).get(index))==false) && (\result==true);
 @ */

改正：

/**@ REQUIRES:None;
 @ MODIFIES:this;
 @ EFFECTS:(\old(this).get(index) !=null) ==> (this.size == \old(this).size-1) && (this.contains(\old(this).get(index))==false) && (\result==true);
 (\old(this).size ==0)==>exceptional_behavior(InvalidRemoveException);
 (index >=\old(this).size) ==> exceptional_behavior (InvalidRemoveException);
 (index < 0) ==> exceptional_behavior (InvalidRemoveException);
 @ */

五、EFFECTS寫得不完整

/**@ REQUIRES:None;
 @ MODIFIES:queue,head;
 @ EFFECTS:\result == queue[head];
 @ THREAD_REQUIRES:None;
 @ THREAD_EFFECTS:None;
 @ */

改正：

/**@ REQUIRES:None;
 @ MODIFIES:queue,head;
 @ EFFECTS:(\result == queue[head])&&(head == \old(head) + 1);
 @ THREAD_REQUIRES:None;
 @ THREAD_EFFECTS:None;
 @ */

 

5、功能bug與規格bug在方法上的彙集關係

	功能bug	規格bug
public long gettime(int i)	0	1(REQUIRES不全，i有範圍)
public synchronized void setflow(int x,int y,int i)	0	1(已經加鎖的方法，沒有在JSF中說明出對應這一點)
大多數run函數	0	1(天然語言)
Driver類的run函數	1(sleep延遲)	1(天然語言，同上)

 

 

 

 

 

多是測試者測得不夠認真，都沒有給我找幾個功能bug，幾乎全是規格bug，所以很難看出功能bug與規格bug在方法上的彙集關係。

 

6、設計規格和撰寫規格的基本思路和體會

一、基本思路

設計規格的時候要保證寫得儘可能簡潔，作到每一個方法只作一件事，這樣在才能保證不會寫出幾百行長的超級方法，可是個人代碼中仍然存在幾百行長的超級方法，例如Driver類的run方法，由於當時寫的時候沒有要求規格，因此寫得洋洋灑灑，後來也很差改了。寫規格的時候要避免使用天然語言，例如隊列的相關操做能夠用contains和size等語言描述其EFFECTS。

二、體會

必定要先設計規格再寫代碼，訓練本身設計規格和按照規格寫代碼的能力，先設計規格再寫代碼還能使代碼寫得更漂亮。