規格化設計-----JSF(第三次博客做業)

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

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

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

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

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

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

從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

至於爲何獲得了人們的重視:我覺的是由於寫出來的代碼要有普遍的使用價值纔是好代碼,而普遍的適用性則要求必需要有相對統一的標準格式,這樣有利於程序員之間溝通交流。

第九次做業的代碼規格使用了天然語言來實現,沒有說明性,就不列出來了。

第十次的代碼有兩個格式錯誤,

1.

public Mypoint(int x, int y) {
/**
* @REQUIRES:None;
* @MODIFIES:None;
* @EFFECTS:實例化一個對象並設置相應參數
*/
super(x,y);
this.x=x;
this.y=y;
this.link=new char[4];
link[0]='f'; //up
link[1]='f'; //right
link[2]='f'; //down
link[3]='f'; //left
p = new Vector<Point>();
}

對於類的初始化方法中MODIFIES應該爲this,而我寫了None;

2.

public void setcredit(int credit) {
/**
* @REQUIRES:None;
* @MODIFIES:this.credit;
* @EFFECTS:this.credit==credit;
*/
this.credit=credit;
}

該方法的前置條件REQUIRES不完整,credit應該約束一個範圍。

 

功能bug與這兩個格式bug無關。

 

功能bug:

字符串轉數字crash,沒有捕捉。

出租車會走回頭路,也就是流量設置有問題,或者道路選擇有問題。

派單時,對於兩個相同起點的乘車請求,雖然出租車被派單,但有一個不會被接單。

在非十字路口設置紅綠燈,沒作報錯處理。(至於要不要作報錯處理,我一頭霧水,助教,issues, 一天變一次,而後本身沒勤刷聊天記錄,信息更新不及時)

測試者在地圖文件裏多添加幾個空格,被提供的GUI類認定爲非法地圖文件並退出

 

第十一次做業:

規格bug

我將GUI提供的一個類單獨成一個類文件,而後沒寫規格,報了兩個規格bug.

一個類沒寫overview, 一個類的repOK寫錯了。

功能bug:

不是最短路徑

路徑字符串限制了長度沒在readme中說明

紅綠燈只能加在十字路口

 

 

 

功能bug與規格bug之間沒有明顯的聯繫,方法多爲獲取類的屬性或者設置類的屬性或者簡單的運算,所以也沒有什麼明顯的改進。

 

撰寫規格的體會:

1.要懂得均衡方法的長度,太長了,規格不太好寫,就像老師說的,多餘50行的方法很難寫出規格。而個人方法就沒掌握好長度,零散的方法比較多,都是set, get方法,要麼就是方法很長,好比有的run方法超過了100行,根本無法規格。

2.代碼的規格頗有必要,若是不寫規格,其餘程序員很難理解方法的目的和相關要求,在團隊合做中這顯得尤其重要。能夠說規格至關於第二天然語言,便於溝通。

相關文章
相關標籤/搜索