第三次博客

第三次博客

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）

2、 bug統計及分析

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

分析：

本身使用的天然語言太多，就不能很好的知足條件，並且，有些規格覺得能夠不寫，就沒寫，好比repok。

 

3、 規格舉例

　　１、使用天然語言　

/** @REQUIRES: r!=null

*@MODIFIES: this
*@EFFECTS: 給this裏的變量賦值
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/

修改後：

/** @REQUIRES: r!=null
*@MODIFIES: this
*@EFFECTS: this!=null
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/

 

　　2、前置條件必須爲布爾表達式

　　　/** @REQUIRES: r範圍爲0-300

*@MODIFIES: this
*@EFFECTS:  this!=null

*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/

修改後：

/** @REQUIRES: 0<=r<300
*@MODIFIES: this
*@EFFECTS: this!=null
*@THREAD_REQUIRES:
*@THREAD_EFFECTS:
*/

 

　　三、忽略了effects　　　

　      　/**@REQUIRES: 
　　　     *@MODIFIES: 
　　　 　*@EFFECTS:None

*@THREAD_REQUIRES:
　　　 　*@THREAD_EFFECTS:
　　　 　*/

　　改進後:

　      　/**@REQUIRES: 
　　　     *@MODIFIES: 
　　　 　*@EFFECTS:\result==>value

　　　 　*@THREAD_REQUIRES:
　　　 　*@THREAD_EFFECTS:
　　　 　*/

　　四、effect直接使用代碼。

　　　　/** @ REQUIRES: r!=null
　　　　@ MODIFIES: this
　　　　@ EFFECTS: r=r+1
　　　　@ THREAD_REQUIRES:
　　　　@ THREAD_EFFECTS:
　　　　@ */

　　　　改進後:

　　　　/** @ REQUIRES: r!==null
　　　　@ MODIFIES: this
　　　　@ EFFECTS: r==old(r)+1
　　　　@ THREAD_REQUIRES:
　　　　@ THREAD_EFFECTS:
　　　　@ */

4、 聚焦關係

基本沒有什麼關係。

5、 思路體會

之後要更深刻地理解規格，不用天然語言，爲了提升代碼質量而寫規格，爲了提高本身而去學習，讓本身在這些方面變得完美。